---

Step * of Lemma mFOL-induction

∀[P:mFOL() ─→ ℙ]
  ((∀name:Atom. ∀vars:ℤ List.  P[name(vars)])
  ⇒ (∀knd:Atom. ∀left,right:mFOL().  (P[left] ⇒ P[right] ⇒ P[mFOconnect(knd;left;right)]))
  ⇒ (∀isall:𝔹. ∀var:ℤ. ∀body:mFOL().  (P[body] ⇒ P[mFOquant(isall;var;body)]))
  ⇒ {∀v:mFOL(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[P:mFOL()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}name:Atom.  \mforall{}vars:\mBbbZ{}  List.    P[name(vars)])
    {}\mRightarrow{}  (\mforall{}knd:Atom.  \mforall{}left,right:mFOL().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[mFOconnect(knd;left;right)]))
    {}\mRightarrow{}  (\mforall{}isall:\mBbbB{}.  \mforall{}var:\mBbbZ{}.  \mforall{}body:mFOL().    (P[body]  {}\mRightarrow{}  P[mFOquant(isall;var;body)]))
    {}\mRightarrow{}  \{\mforall{}v:mFOL().  P[v]\})


By

ProveDatatypeInd

---

Home Index