---

Step * of Lemma RankEx1-induction

∀[T:Type]. ∀[P:RankEx1(T) ─→ ℙ].
  ((∀leaf:T. P[RankEx1_Leaf(leaf)])
  ⇒ (∀prod:RankEx1(T) × RankEx1(T). (let u,u1 = prod in P[u] ∧ P[u1] ⇒ P[RankEx1_Prod(prod)]))
  ⇒ (∀prodl:T × RankEx1(T). (let u,u1 = prodl in P[u1] ⇒ P[RankEx1_ProdL(prodl)]))
  ⇒ (∀prodr:RankEx1(T) × T. (let u,u1 = prodr in P[u] ⇒ P[RankEx1_ProdR(prodr)]))
  ⇒ (∀list:RankEx1(T) List. ((∀u∈list.P[u]) ⇒ P[RankEx1_List(list)]))
  ⇒ {∀v:RankEx1(T). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[T:Type].  \mforall{}[P:RankEx1(T)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}leaf:T.  P[RankEx1\_Leaf(leaf)])
    {}\mRightarrow{}  (\mforall{}prod:RankEx1(T)  \mtimes{}  RankEx1(T).  (let  u,u1  =  prod  in  P[u]  \mwedge{}  P[u1]  {}\mRightarrow{}  P[RankEx1\_Prod(prod)]))
    {}\mRightarrow{}  (\mforall{}prodl:T  \mtimes{}  RankEx1(T).  (let  u,u1  =  prodl  in  P[u1]  {}\mRightarrow{}  P[RankEx1\_ProdL(prodl)]))
    {}\mRightarrow{}  (\mforall{}prodr:RankEx1(T)  \mtimes{}  T.  (let  u,u1  =  prodr  in  P[u]  {}\mRightarrow{}  P[RankEx1\_ProdR(prodr)]))
    {}\mRightarrow{}  (\mforall{}list:RankEx1(T)  List.  ((\mforall{}u\mmember{}list.P[u])  {}\mRightarrow{}  P[RankEx1\_List(list)]))
    {}\mRightarrow{}  \{\mforall{}v:RankEx1(T).  P[v]\})


By

ProveDatatypeInd

---

Home Index