---

Step * of Lemma int_formula-definition

∀[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ].
  ((∀left,right:int_term().  {x:A| R[x;(left "<" right)]} )
  ⇒ (∀left,right:int_term().  {x:A| R[x;left "≤" right]} )
  ⇒ (∀left,right:int_term().  {x:A| R[x;left "=" right]} )
  ⇒ (∀left,right:int_formula().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left "∧" right]} ))
  ⇒ (∀left,right:int_formula().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left "or" right]} ))
  ⇒ (∀left,right:int_formula().  ({x:A| R[x;left]}  ⇒ {x:A| R[x;right]}  ⇒ {x:A| R[x;left "=>" right]} ))
  ⇒ (∀form:int_formula(). ({x:A| R[x;form]}  ⇒ {x:A| R[x;"¬"form]} ))
  ⇒ {∀v:int_formula(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `int_formula-induction` }

---

Latex:

---

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


By

---

Latex:
ProveDatatypeDefinition  `int\_formula-induction`

---

Home Index