---

Step * of Lemma Form-definition

∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ].
  ((∀name:Atom. {x:A| R[x;Vname]} )
  ⇒ (∀value:C. {x:A| R[x;Const(value)]} )
  ⇒ (∀var:Atom. ∀phi:Form(C).  ({x:A| R[x;phi]}  ⇒ {x:A| R[x;{var | phi}]} ))
  ⇒ (∀left,right:Form(C).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left = right]} ))
  ⇒ (∀element,set:Form(C).  ({x:A| R[x;element]}  ⇒ {x:A| R[x;set]}  ⇒ {x:A| R[x;element ∈ set]} ))
  ⇒ (∀left,right:Form(C).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left ∧ right)]} ))
  ⇒ (∀left,right:Form(C).  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left ∨ right]} ))
  ⇒ (∀body:Form(C). ({x:A| R[x;body]}  ⇒ {x:A| R[x;¬(body)]} ))
  ⇒ (∀var:Atom. ∀body:Form(C).  ({x:A| R[x;body]}  ⇒ {x:A| R[x;∀var. body]} ))
  ⇒ (∀var:Atom. ∀body:Form(C).  ({x:A| R[x;body]}  ⇒ {x:A| R[x;∃var. body]} ))
  ⇒ {∀v:Form(C). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `Form-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `Form-induction`

---

Home Index