---

Step * of Lemma formula-induction

∀[P:formula() ⟶ ℙ]
  ((∀name:Atom. P[pvar(name)])
  ⇒ (∀sub:formula(). (P[sub] ⇒ P[pnot(sub)]))
  ⇒ (∀left,right:formula().  (P[left] ⇒ P[right] ⇒ P[pand(left;right)]))
  ⇒ (∀left,right:formula().  (P[left] ⇒ P[right] ⇒ P[por(left;right)]))
  ⇒ (∀left,right:formula().  (P[left] ⇒ P[right] ⇒ P[pimp(left;right)]))
  ⇒ {∀v:formula(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeInd

---

Home Index