---

Step * of Lemma mFOL-definition

∀[A:Type]. ∀[R:A ─→ mFOL() ─→ ℙ].
  ((∀name:Atom. ∀vars:ℤ List.  {x:A| R[x;name(vars)]} )
  ⇒ (∀knd:Atom. ∀left,right:mFOL().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;mFOconnect(knd;left;right)]}\000C ))
  ⇒ (∀isall:𝔹. ∀var:ℤ. ∀body:mFOL().  ({x:A| R[x;body]}  ⇒ {x:A| R[x;mFOquant(isall;var;body)]} ))
  ⇒ {∀v:mFOL(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `mFOL-induction` }

---

Latex:


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


By

ProveDatatypeDefinition  `mFOL-induction`

---

Home Index