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
Definitions unfolded in proof :  RankEx2_ind: RankEx2_ind,  uall: ∀[x:A]. B[x],  member: t ∈ T,  ext-eq: A ≡ B,  and: P ∧ Q,  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  implies: P ⇒ Q,  exposed-it: exposed-it,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  uiff: uiff(P;Q),  uimplies: b supposing a,  sq_type: SQType(T),  guard: {T},  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  RankEx2_LeafT: RankEx2_LeafT(leaft),  so_apply: x[s1;s2],  so_apply: x[s],  let: let,  RankEx2_LeafT?: RankEx2_LeafT?(v),  pi1: fst(t),  RankEx2_LeafT-leaft: RankEx2_LeafT-leaft(v),  RankEx2_LeafS?: RankEx2_LeafS?(v),  RankEx2_LeafS-leafs: RankEx2_LeafS-leafs(v),  RankEx2_Prod?: RankEx2_Prod?(v),  RankEx2_Prod-prod: RankEx2_Prod-prod(v),  RankEx2_Union?: RankEx2_Union?(v),  RankEx2_Union-union: RankEx2_Union-union(v),  RankEx2_ListProd?: RankEx2_ListProd?(v),  RankEx2_ListProd-listprod: RankEx2_ListProd-listprod(v),  RankEx2_UnionList-unionlist: RankEx2_UnionList-unionlist(v),  pi2: snd(t),  bfalse: ff,  exists: ∃x:A. B[x],  prop: ℙ,  or: P ∨ Q,  bnot: ¬bb,  assert: ↑b,  false: False,  RankEx2_LeafS: RankEx2_LeafS(leafs),  RankEx2_Prod: RankEx2_Prod(prod),  RankEx2_Union: RankEx2_Union(union),  RankEx2_ListProd: RankEx2_ListProd(listprod),  RankEx2_UnionList: RankEx2_UnionList(unionlist)
Lemmas referenced :  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
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  cut,  lemma_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  promote_hyp,  productElimination,  hypothesis_subsumption,  hypothesis,  applyEquality,  tokenEquality,  lambdaFormation,  unionElimination,  equalityElimination,  equalityTransitivity,  equalitySymmetry,  independent_isectElimination,  instantiate,  cumulativity,  atomEquality,  dependent_functionElimination,  independent_functionElimination,  because_Cache,  dependent_pairFormation,  voidElimination,  equalityEquality,  functionEquality,  universeEquality,  isect_memberFormation,  introduction,  sqequalAxiom,  isect_memberEquality
Latex:
\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: 2016_05_16-AM-09_02_55
Last ObjectModification: 2015_12_28-PM-06_50_04

Theory : C-semantics


Home Index