---

Step * of Lemma mFOLRule-induction

∀[P:mFOLRule() ─→ ℙ]
  (P[andI]
  ⇒ P[impI]
  ⇒ (∀var:ℤ. P[allI with var])
  ⇒ (∀var:ℤ. P[existsI with var])
  ⇒ (∀left:𝔹. P[mRuleorI(left)])
  ⇒ P[hyp]
  ⇒ (∀hypnum:ℕ. P[andE on hypnum])
  ⇒ (∀hypnum:ℕ. P[orE on hypnum])
  ⇒ (∀hypnum:ℕ. P[impE on hypnum])
  ⇒ (∀hypnum:ℕ. ∀var:ℤ.  P[allE on hypnum with var])
  ⇒ (∀hypnum:ℕ. ∀var:ℤ.  P[existsE on hypnum with var])
  ⇒ {∀v:mFOLRule(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


\mforall{}[P:mFOLRule()  {}\mrightarrow{}  \mBbbP{}]
    (P[andI]
    {}\mRightarrow{}  P[impI]
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[allI  with  var])
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[existsI  with  var])
    {}\mRightarrow{}  (\mforall{}left:\mBbbB{}.  P[mRuleorI(left)])
    {}\mRightarrow{}  P[hyp]
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[andE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[orE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  P[impE  on  hypnum])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    P[allE  on  hypnum  with  var])
    {}\mRightarrow{}  (\mforall{}hypnum:\mBbbN{}.  \mforall{}var:\mBbbZ{}.    P[existsE  on  hypnum  with  var])
    {}\mRightarrow{}  \{\mforall{}v:mFOLRule().  P[v]\})


By

ProveDatatypeInd

---

Home Index