Nuprl Lemma : RankEx2-induction

[S,T:Type]. ∀[P:RankEx2(S;T) ─→ ℙ].
  ((∀leaft:T. P[RankEx2_LeafT(leaft)])
   (∀leafs:S. P[RankEx2_LeafS(leafs)])
   (∀prod:RankEx2(S;T) × S × T. (let u,u1 prod in let u1,u2 in P[u1]  P[RankEx2_Prod(prod)]))
   (∀union:S × RankEx2(S;T) RankEx2(S;T)
        (case union of inl(u) => let u1,u2 in P[u2] inr(u1) => P[u1]  P[RankEx2_Union(union)]))
   (∀listprod:(S × RankEx2(S;T)) List. ((∀u∈listprod.let u1,u2 in P[u2])  P[RankEx2_ListProd(listprod)]))
   (∀unionlist:T (RankEx2(S;T) List)
        (case unionlist of inl(u) => True inr(u1) => (∀u∈u1.P[u])  P[RankEx2_UnionList(unionlist)]))
   {∀v:RankEx2(S;T). P[v]})


Definitions occuring in Statement :  RankEx2_UnionList: RankEx2_UnionList(unionlist) RankEx2_ListProd: RankEx2_ListProd(listprod) RankEx2_Union: RankEx2_Union(union) RankEx2_Prod: RankEx2_Prod(prod) RankEx2_LeafS: RankEx2_LeafS(leafs) RankEx2_LeafT: RankEx2_LeafT(leaft) RankEx2: RankEx2(S;T) l_all: (∀x∈L.P[x]) list: List uall: [x:A]. B[x] prop: guard: {T} so_apply: x[s] all: x:A. B[x] implies:  Q true: True function: x:A ─→ B[x] spread: spread def product: x:A × B[x] decide: case of inl(x) => s[x] inr(y) => t[y] union: left right universe: Type
Lemmas :  uniform-comp-nat-induction all_wf isect_wf le_wf RankEx2_size_wf nat_wf less_than_wf RankEx2-ext eq_atom_wf bool_wf eqtt_to_assert assert_of_eq_atom subtype_base_sq atom_subtype_base eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_atom decidable__lt false_wf add_functionality_wrt_le add-swap add-commutes le-add-cancel subtract_wf decidable__le not-le-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-zero subtract-is-less lelt_wf sum-nat length_wf_nat select_wf sq_stable__le int_seg_wf length_wf sum_wf RankEx2_wf sum-nat-less uall_wf le_weakening list_wf true_wf l_all_wf2 l_member_wf RankEx2_UnionList_wf RankEx2_ListProd_wf RankEx2_Union_wf RankEx2_Prod_wf RankEx2_LeafS_wf RankEx2_LeafT_wf
\mforall{}[S,T:Type].  \mforall{}[P:RankEx2(S;T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}leaft:T.  P[RankEx2\_LeafT(leaft)])
    {}\mRightarrow{}  (\mforall{}leafs:S.  P[RankEx2\_LeafS(leafs)])
    {}\mRightarrow{}  (\mforall{}prod:RankEx2(S;T)  \mtimes{}  S  \mtimes{}  T
                (let  u,u1  =  prod  in  let  u1,u2  =  u  in  P[u1]  {}\mRightarrow{}  P[RankEx2\_Prod(prod)]))
    {}\mRightarrow{}  (\mforall{}union:S  \mtimes{}  RankEx2(S;T)  +  RankEx2(S;T)
                (case  union  of  inl(u)  =>  let  u1,u2  =  u  in  P[u2]  |  inr(u1)  =>  P[u1]
                {}\mRightarrow{}  P[RankEx2\_Union(union)]))
    {}\mRightarrow{}  (\mforall{}listprod:(S  \mtimes{}  RankEx2(S;T))  List
                ((\mforall{}u\mmember{}listprod.let  u1,u2  =  u  in  P[u2])  {}\mRightarrow{}  P[RankEx2\_ListProd(listprod)]))
    {}\mRightarrow{}  (\mforall{}unionlist:T  +  (RankEx2(S;T)  List)
                (case  unionlist  of  inl(u)  =>  True  |  inr(u1)  =>  (\mforall{}u\mmember{}u1.P[u])
                {}\mRightarrow{}  P[RankEx2\_UnionList(unionlist)]))
    {}\mRightarrow{}  \{\mforall{}v:RankEx2(S;T).  P[v]\})

Date html generated: 2015_07_17-AM-07_50_15
Last ObjectModification: 2015_01_27-AM-09_38_08

Home Index