---

Step * of Lemma int_term-definition

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

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `int\_term-induction`

---

Home Index