---

Step * of Lemma rat_term-induction

∀[P:rat_term() ⟶ ℙ]
  ((∀const:ℤ. P["const"])
  ⇒ (∀var:ℤ. P[rtermVar(var)])
  ⇒ (∀left,right:rat_term().  (P[left] ⇒ P[right] ⇒ P[left "+" right]))
  ⇒ (∀left,right:rat_term().  (P[left] ⇒ P[right] ⇒ P[left "-" right]))
  ⇒ (∀left,right:rat_term().  (P[left] ⇒ P[right] ⇒ P[left "*" right]))
  ⇒ (∀num,denom:rat_term().  (P[num] ⇒ P[denom] ⇒ P[num "/" denom]))
  ⇒ (∀num:rat_term(). (P[num] ⇒ P[rtermMinus(num)]))
  ⇒ {∀v:rat_term(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeInd

---

Home Index