---

Step * of Lemma rat_term-definition

∀[A:Type]. ∀[R:A ⟶ rat_term() ⟶ ℙ].
  ((∀const:ℤ. {x:A| R[x;"const"]} )
  ⇒ (∀var:ℤ. {x:A| R[x;rtermVar(var)]} )
  ⇒ (∀left,right:rat_term().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left "+" right]} ))
  ⇒ (∀left,right:rat_term().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left "-" right]} ))
  ⇒ (∀left,right:rat_term().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left "*" right]} ))
  ⇒ (∀num,denom:rat_term().  ({x:A| R[x;num]}  ⇒ {x:A| R[x;denom]}  ⇒ {x:A| R[x;num "/" denom]} ))
  ⇒ (∀num:rat_term(). ({x:A| R[x;num]}  ⇒ {x:A| R[x;rtermMinus(num)]} ))
  ⇒ {∀v:rat_term(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `rat_term-induction` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  rat\_term()  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}const:\mBbbZ{}.  \{x:A|  R[x;"const"]\}  )
    {}\mRightarrow{}  (\mforall{}var:\mBbbZ{}.  \{x:A|  R[x;rtermVar(var)]\}  )
    {}\mRightarrow{}  (\mforall{}left,right:rat\_term().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;left  "+"  right]\}  ))
    {}\mRightarrow{}  (\mforall{}left,right:rat\_term().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;left  "-"  right]\}  ))
    {}\mRightarrow{}  (\mforall{}left,right:rat\_term().
                (\{x:A|  R[x;left]\}    {}\mRightarrow{}  \{x:A|  R[x;right]\}    {}\mRightarrow{}  \{x:A|  R[x;left  "*"  right]\}  ))
    {}\mRightarrow{}  (\mforall{}num,denom:rat\_term().    (\{x:A|  R[x;num]\}    {}\mRightarrow{}  \{x:A|  R[x;denom]\}    {}\mRightarrow{}  \{x:A|  R[x;num  "/"  denom]\}  )\000C)
    {}\mRightarrow{}  (\mforall{}num:rat\_term().  (\{x:A|  R[x;num]\}    {}\mRightarrow{}  \{x:A|  R[x;rtermMinus(num)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:rat\_term().  \{x:A|  R[x;v]\}  \})


By

---

Latex:
ProveDatatypeDefinition  `rat\_term-induction`

---

Home Index