---

Step * of Lemma formula-definition

∀[A:Type]. ∀[R:A ⟶ formula() ⟶ ℙ].
  ((∀name:Atom. {x:A| R[x;pvar(name)]} )
  ⇒ (∀sub:formula(). ({x:A| R[x;sub]}  ⇒ {x:A| R[x;pnot(sub)]} ))
  ⇒ (∀left,right:formula().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;pand(left;right)]} ))
  ⇒ (∀left,right:formula().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;por(left;right)]} ))
  ⇒ (∀left,right:formula().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;pimp(left;right)]} ))
  ⇒ {∀v:formula(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `formula-induction` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  formula()  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}name:Atom.  \{x:A|  R[x;pvar(name)]\}  )
    {}\mRightarrow{}  (\mforall{}sub:formula().  (\{x:A|  R[x;sub]\}    {}\mRightarrow{}  \{x:A|  R[x;pnot(sub)]\}  ))
    {}\mRightarrow{}  (\mforall{}left,right:formula().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;pand(left;right)]\}  ))
    {}\mRightarrow{}  (\mforall{}left,right:formula().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;por(left;right)]\}  ))
    {}\mRightarrow{}  (\mforall{}left,right:formula().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;pimp(left;right)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:formula().  \{x:A|  R[x;v]\}  \})


By

---

Latex:
ProveDatatypeDefinition  `formula-induction`

---

Home Index