Nuprl Lemma : RankEx2_ind-unroll

∀[S,T,A:Type]. ∀[R:A ─→ RankEx2(S;T) ─→ ℙ]. ∀[LeafT,LeafS,Prod,Union,ListProd,UnionList:Top]. ∀[t:RankEx2(S;T)].
  (RankEx2_ind(t;
               RankEx2_LeafT(leaft)⇒ LeafT[leaft];
               RankEx2_LeafS(leafs)⇒ LeafS[leafs];
               RankEx2_Prod(prod)⇒ rec1.Prod[prod;rec1];
               RankEx2_Union(union)⇒ rec2.Union[union;rec2];
               RankEx2_ListProd(listprod)⇒ rec3.ListProd[listprod;rec3];
               RankEx2_UnionList(unionlist)⇒ rec4.UnionList[unionlist;rec4])  
  ~ let F = λt.RankEx2_ind(t;
                           RankEx2_LeafT(leaft)⇒ LeafT[leaft];
                           RankEx2_LeafS(leafs)⇒ LeafS[leafs];
                           RankEx2_Prod(prod)⇒ rec1.Prod[prod;rec1];
                           RankEx2_Union(union)⇒ rec2.Union[union;rec2];
                           RankEx2_ListProd(listprod)⇒ rec3.ListProd[listprod;rec3];
                           RankEx2_UnionList(unionlist)⇒ rec4.UnionList[unionlist;rec4])  in
        if RankEx2_LeafT?(t) then LeafT RankEx2_LeafT-leaft(t)
        if RankEx2_LeafS?(t) then LeafS RankEx2_LeafS-leafs(t)
        if RankEx2_Prod?(t) then Prod RankEx2_Prod-prod(t) (F (fst(fst(RankEx2_Prod-prod(t)))))
        if RankEx2_Union?(t)
          then Union RankEx2_Union-union(t) 
               case RankEx2_Union-union(t) of inl(x) => let x1,x2 = x in F x2 | inr(y) => F y
        if RankEx2_ListProd?(t)
          then ListProd RankEx2_ListProd-listprod(t) (λi.let u2,u3 = RankEx2_ListProd-listprod(t)[i] in F u3)
        else UnionList RankEx2_UnionList-unionlist(t) 
             case RankEx2_UnionList-unionlist(t) of inl(x) => Ax | inr(y) => λi.(F y[i])
        fi )


Proof



Definitions occuring in Statement :  RankEx2_ind: RankEx2_ind,  RankEx2_UnionList-unionlist: RankEx2_UnionList-unionlist(v),  RankEx2_ListProd-listprod: RankEx2_ListProd-listprod(v),  RankEx2_ListProd?: RankEx2_ListProd?(v),  RankEx2_Union-union: RankEx2_Union-union(v),  RankEx2_Union?: RankEx2_Union?(v),  RankEx2_Prod-prod: RankEx2_Prod-prod(v),  RankEx2_Prod?: RankEx2_Prod?(v),  RankEx2_LeafS-leafs: RankEx2_LeafS-leafs(v),  RankEx2_LeafS?: RankEx2_LeafS?(v),  RankEx2_LeafT-leaft: RankEx2_LeafT-leaft(v),  RankEx2_LeafT?: RankEx2_LeafT?(v),  RankEx2: RankEx2(S;T),  select: L[n],  ifthenelse: if b then t else f fi ,  let: let,  uall: ∀[x:A]. B[x],  top: Top,  prop: ℙ,  so_apply: x[s1;s2],  so_apply: x[s],  pi1: fst(t),  apply: f a,  lambda: λx.A[x],  function: x:A ─→ B[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  universe: Type,  sqequal: s ~ t,  axiom: Ax
Lemmas :  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,  RankEx2_wf,  top_wf
\mforall{}[S,T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx2(S;T)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[LeafT,LeafS,Prod,Union,ListProd,UnionList:Top].
\mforall{}[t:RankEx2(S;T)].
    (RankEx2\_ind(t;
                              RankEx2\_LeafT(leaft){}\mRightarrow{}  LeafT[leaft];
                              RankEx2\_LeafS(leafs){}\mRightarrow{}  LeafS[leafs];
                              RankEx2\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                              RankEx2\_Union(union){}\mRightarrow{}  rec2.Union[union;rec2];
                              RankEx2\_ListProd(listprod){}\mRightarrow{}  rec3.ListProd[listprod;rec3];
                              RankEx2\_UnionList(unionlist){}\mRightarrow{}  rec4.UnionList[unionlist;rec4])   
    \msim{}  let  F  =  \mlambda{}t.RankEx2\_ind(t;
                                                      RankEx2\_LeafT(leaft){}\mRightarrow{}  LeafT[leaft];
                                                      RankEx2\_LeafS(leafs){}\mRightarrow{}  LeafS[leafs];
                                                      RankEx2\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                                                      RankEx2\_Union(union){}\mRightarrow{}  rec2.Union[union;rec2];
                                                      RankEx2\_ListProd(listprod){}\mRightarrow{}  rec3.ListProd[listprod;rec3];
                                                      RankEx2\_UnionList(unionlist){}\mRightarrow{}  rec4.UnionList[unionlist;rec4])    in
                if  RankEx2\_LeafT?(t)  then  LeafT  RankEx2\_LeafT-leaft(t)
                if  RankEx2\_LeafS?(t)  then  LeafS  RankEx2\_LeafS-leafs(t)
                if  RankEx2\_Prod?(t)  then  Prod  RankEx2\_Prod-prod(t)  (F  (fst(fst(RankEx2\_Prod-prod(t)))))
                if  RankEx2\_Union?(t)
                    then  Union  RankEx2\_Union-union(t) 
                              case  RankEx2\_Union-union(t)  of  inl(x)  =>  let  x1,x2  =  x  in  F  x2  |  inr(y)  =>  F  y
                if  RankEx2\_ListProd?(t)
                    then  ListProd  RankEx2\_ListProd-listprod(t) 
                              (\mlambda{}i.let  u2,u3  =  RankEx2\_ListProd-listprod(t)[i] 
                                      in  F  u3)
                else  UnionList  RankEx2\_UnionList-unionlist(t) 
                          case  RankEx2\_UnionList-unionlist(t)  of  inl(x)  =>  Ax  |  inr(y)  =>  \mlambda{}i.(F  y[i])
                fi  )


Date html generated: 2015_07_17-AM-07_50_29
Last ObjectModification: 2015_01_27-AM-09_36_54

Home Index