---

Step * of Lemma int_formula-induction

∀[P:int_formula() ⟶ ℙ]
  ((∀left,right:int_term().  P[(left "<" right)])
  ⇒ (∀left,right:int_term().  P[left "≤" right])
  ⇒ (∀left,right:int_term().  P[left "=" right])
  ⇒ (∀left,right:int_formula().  (P[left] ⇒ P[right] ⇒ P[left "∧" right]))
  ⇒ (∀left,right:int_formula().  (P[left] ⇒ P[right] ⇒ P[left "or" right]))
  ⇒ (∀left,right:int_formula().  (P[left] ⇒ P[right] ⇒ P[left "=>" right]))
  ⇒ (∀form:int_formula(). (P[form] ⇒ P["¬"form]))
  ⇒ {∀v:int_formula(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[P:int\_formula()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}left,right:int\_term().    P[(left  "<"  right)])
    {}\mRightarrow{}  (\mforall{}left,right:int\_term().    P[left  "\mleq{}"  right])
    {}\mRightarrow{}  (\mforall{}left,right:int\_term().    P[left  "="  right])
    {}\mRightarrow{}  (\mforall{}left,right:int\_formula().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  "\mwedge{}"  right]))
    {}\mRightarrow{}  (\mforall{}left,right:int\_formula().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  "or"  right]))
    {}\mRightarrow{}  (\mforall{}left,right:int\_formula().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  "=>"  right]))
    {}\mRightarrow{}  (\mforall{}form:int\_formula().  (P[form]  {}\mRightarrow{}  P["\mneg{}"form]))
    {}\mRightarrow{}  \{\mforall{}v:int\_formula().  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index