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:
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
Latex:
ProveDatatypeInd
Home
Index