---

Step * of Lemma RankEx1_ind_wf

∀[T,A:Type]. ∀[R:A ─→ RankEx1(T) ─→ ℙ]. ∀[v:RankEx1(T)]. ∀[Leaf:leaf:T ─→ {x:A| R[x;RankEx1_Leaf(leaf)]} ].
∀[Prod:prod:(RankEx1(T) × RankEx1(T))
       ─→ let u,u1 = prod 
          in {x:A| R[x;u]}  ∧ {x:A| R[x;u1]} 
       ─→ {x:A| R[x;RankEx1_Prod(prod)]} ]. ∀[ProdL:prodl:(T × RankEx1(T))
                                                   ─→ let u,u1 = prodl 
                                                      in {x:A| R[x;u1]} 
                                                   ─→ {x:A| R[x;RankEx1_ProdL(prodl)]} ].
∀[ProdR:prodr:(RankEx1(T) × T) ─→ let u,u1 = prodr in {x:A| R[x;u]}  ─→ {x:A| R[x;RankEx1_ProdR(prodr)]} ].
∀[List:list:(RankEx1(T) List) ─→ (∀u∈list.{x:A| R[x;u]} ) ─→ {x:A| R[x;RankEx1_List(list)]} ].
  (RankEx1_ind(v;
               RankEx1_Leaf(leaf)⇒ Leaf[leaf];
               RankEx1_Prod(prod)⇒ rec1.Prod[prod;rec1];
               RankEx1_ProdL(prodl)⇒ rec2.ProdL[prodl;rec2];
               RankEx1_ProdR(prodr)⇒ rec3.ProdR[prodr;rec3];
               RankEx1_List(list)⇒ rec4.List[list;rec4])  ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{RankEx1-definition:o, 1:l, i:l}⋅ }

---

Latex:


\mforall{}[T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx1(T)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:RankEx1(T)].  \mforall{}[Leaf:leaf:T  {}\mrightarrow{}  \{x:A| 
                                                                                                                                                      R
                                                                                                                                                      [x;RankEx1\_Leaf(leaf)]\}  ]\000C.
\mforall{}[Prod:prod:(RankEx1(T)  \mtimes{}  RankEx1(T))
              {}\mrightarrow{}  let  u,u1  =  prod 
                    in  \{x:A|  R[x;u]\}    \mwedge{}  \{x:A|  R[x;u1]\} 
              {}\mrightarrow{}  \{x:A|  R[x;RankEx1\_Prod(prod)]\}  ].  \mforall{}[ProdL:prodl:(T  \mtimes{}  RankEx1(T))
                                                                                                      {}\mrightarrow{}  let  u,u1  =  prodl 
                                                                                                            in  \{x:A|  R[x;u1]\} 
                                                                                                      {}\mrightarrow{}  \{x:A|  R[x;RankEx1\_ProdL(prodl)]\}  ].
\mforall{}[ProdR:prodr:(RankEx1(T)  \mtimes{}  T)
                {}\mrightarrow{}  let  u,u1  =  prodr 
                      in  \{x:A|  R[x;u]\} 
                {}\mrightarrow{}  \{x:A|  R[x;RankEx1\_ProdR(prodr)]\}  ].  \mforall{}[List:list:(RankEx1(T)  List)
                                                                                                          {}\mrightarrow{}  (\mforall{}u\mmember{}list.\{x:A|  R[x;u]\}  )
                                                                                                          {}\mrightarrow{}  \{x:A|  R[x;RankEx1\_List(list)]\}  ].
    (RankEx1\_ind(v;
                              RankEx1\_Leaf(leaf){}\mRightarrow{}  Leaf[leaf];
                              RankEx1\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                              RankEx1\_ProdL(prodl){}\mRightarrow{}  rec2.ProdL[prodl;rec2];
                              RankEx1\_ProdR(prodr){}\mRightarrow{}  rec3.ProdR[prodr;rec3];
                              RankEx1\_List(list){}\mRightarrow{}  rec4.List[list;rec4])    \mmember{}  \{x:A|  R[x;v]\}  )


By

ProveDatatypeIndWf  TERMOF\{RankEx1-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index