---

Step * of Lemma mFOLRule-definition

∀[A:Type]. ∀[R:A ─→ mFOLRule() ─→ ℙ].
  ({x:A| R[x;andI]} 
  ⇒ {x:A| R[x;impI]} 
  ⇒ (∀var:ℤ. {x:A| R[x;allI with var]} )
  ⇒ (∀var:ℤ. {x:A| R[x;existsI with var]} )
  ⇒ (∀left:𝔹. {x:A| R[x;mRuleorI(left)]} )
  ⇒ {x:A| R[x;hyp]} 
  ⇒ (∀hypnum:ℕ. {x:A| R[x;andE on hypnum]} )
  ⇒ (∀hypnum:ℕ. {x:A| R[x;orE on hypnum]} )
  ⇒ (∀hypnum:ℕ. {x:A| R[x;impE on hypnum]} )
  ⇒ (∀hypnum:ℕ. ∀var:ℤ.  {x:A| R[x;allE on hypnum with var]} )
  ⇒ (∀hypnum:ℕ. ∀var:ℤ.  {x:A| R[x;existsE on hypnum with var]} )
  ⇒ {∀v:mFOLRule(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `mFOLRule-induction` }

---

Latex:


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


By

ProveDatatypeDefinition  `mFOLRule-induction`

---

Home Index