---

Step * of Lemma RankEx1-definition

∀[T,A:Type]. ∀[R:A ⟶ RankEx1(T) ⟶ ℙ].
  ((∀leaf:T. {x:A| R[x;RankEx1_Leaf(leaf)]} )
  ⇒ (∀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:T × RankEx1(T). (let u,u1 = prodl in {x:A| R[x;u1]}  ⇒ {x:A| R[x;RankEx1_ProdL(prodl)]} ))
  ⇒ (∀prodr:RankEx1(T) × T. (let u,u1 = prodr in {x:A| R[x;u]}  ⇒ {x:A| R[x;RankEx1_ProdR(prodr)]} ))
  ⇒ (∀list:RankEx1(T) List. ((∀u∈list.{x:A| R[x;u]} ) ⇒ {x:A| R[x;RankEx1_List(list)]} ))
  ⇒ {∀v:RankEx1(T). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `RankEx1-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `RankEx1-induction`

---

Home Index