---

Step * of Lemma Form-induction

∀[C:Type]. ∀[P:Form(C) ⟶ ℙ].
  ((∀name:Atom. P[Vname])
  ⇒ (∀value:C. P[Const(value)])
  ⇒ (∀var:Atom. ∀phi:Form(C).  (P[phi] ⇒ P[{var | phi}]))
  ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left = right]))
  ⇒ (∀element,set:Form(C).  (P[element] ⇒ P[set] ⇒ P[element ∈ set]))
  ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∧ right)]))
  ⇒ (∀left,right:Form(C).  (P[left] ⇒ P[right] ⇒ P[left ∨ right]))
  ⇒ (∀body:Form(C). (P[body] ⇒ P[¬(body)]))
  ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∀var. body]))
  ⇒ (∀var:Atom. ∀body:Form(C).  (P[body] ⇒ P[∃var. body]))
  ⇒ {∀v:Form(C). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[P:Form(C)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}name:Atom.  P[Vname])
    {}\mRightarrow{}  (\mforall{}value:C.  P[Const(value)])
    {}\mRightarrow{}  (\mforall{}var:Atom.  \mforall{}phi:Form(C).    (P[phi]  {}\mRightarrow{}  P[\{var  |  phi\}]))
    {}\mRightarrow{}  (\mforall{}left,right:Form(C).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  =  right]))
    {}\mRightarrow{}  (\mforall{}element,set:Form(C).    (P[element]  {}\mRightarrow{}  P[set]  {}\mRightarrow{}  P[element  \mmember{}  set]))
    {}\mRightarrow{}  (\mforall{}left,right:Form(C).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  \mwedge{}  right)]))
    {}\mRightarrow{}  (\mforall{}left,right:Form(C).    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  \mvee{}  right]))
    {}\mRightarrow{}  (\mforall{}body:Form(C).  (P[body]  {}\mRightarrow{}  P[\mneg{}(body)]))
    {}\mRightarrow{}  (\mforall{}var:Atom.  \mforall{}body:Form(C).    (P[body]  {}\mRightarrow{}  P[\mforall{}var.  body]))
    {}\mRightarrow{}  (\mforall{}var:Atom.  \mforall{}body:Form(C).    (P[body]  {}\mRightarrow{}  P[\mexists{}var.  body]))
    {}\mRightarrow{}  \{\mforall{}v:Form(C).  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index