---

Step * of Lemma int_term-induction

∀[P:int_term() ⟶ ℙ]
  ((∀const:ℤ. P["const"])
  ⇒ (∀var:ℤ. P[vvar])
  ⇒ (∀left,right:int_term().  (P[left] ⇒ P[right] ⇒ P[left (+) right]))
  ⇒ (∀left,right:int_term().  (P[left] ⇒ P[right] ⇒ P[left (-) right]))
  ⇒ (∀left,right:int_term().  (P[left] ⇒ P[right] ⇒ P[left (*) right]))
  ⇒ (∀num:int_term(). (P[num] ⇒ P["-"num]))
  ⇒ {∀v:int_term(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[P:int\_term()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}const:\mBbbZ{}.  P["const"])
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  P[vvar])
    {}\mRightarrow{}  (\mforall{}left,right:int\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  (+)  right]))
    {}\mRightarrow{}  (\mforall{}left,right:int\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  (-)  right]))
    {}\mRightarrow{}  (\mforall{}left,right:int\_term().    (P[left]  {}\mRightarrow{}  P[right]  {}\mRightarrow{}  P[left  (*)  right]))
    {}\mRightarrow{}  (\mforall{}num:int\_term().  (P[num]  {}\mRightarrow{}  P["-"num]))
    {}\mRightarrow{}  \{\mforall{}v:int\_term().  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index