Step * of Lemma int_formula_ind_wf_simple

`∀[A:Type]. ∀[v:int_formula()]. ∀[less,le,eq:left:int_term() ⟶ right:int_term() ⟶ A].`
`∀[and,or,implies:left:int_formula() ⟶ right:int_formula() ⟶ A ⟶ A ⟶ A]. ∀[not:form:int_formula() ⟶ A ⟶ A].`
`  (int_formula_ind(v;`
`                   intformless(left,right)`` less[left;right];`
`                   intformle(left,right)`` le[left;right];`
`                   intformeq(left,right)`` eq[left;right];`
`                   intformand(left,right)`` rec1,rec2.and[left;right;rec1;rec2];`
`                   intformor(left,right)`` rec3,rec4.or[left;right;rec3;rec4];`
`                   intformimplies(left,right)`` rec5,rec6.implies[left;right;rec5;rec6];`
`                   intformnot(form)`` rec7.not[form;rec7])  ∈ A)`
BY
`{ (ProveDatatypeIndWfSimple' int_formula_ind_wf) }`

Latex:

Latex:
\mforall{}[A:Type].  \mforall{}[v:int\_formula()].  \mforall{}[less,le,eq:left:int\_term()  {}\mrightarrow{}  right:int\_term()  {}\mrightarrow{}  A].
\mforall{}[and,or,implies:left:int\_formula()  {}\mrightarrow{}  right:int\_formula()  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].  \mforall{}[not:form:int\_formula()
{}\mrightarrow{}  A
{}\mrightarrow{}  A].
(int\_formula\_ind(v;
intformless(left,right){}\mRightarrow{}  less[left;right];
intformle(left,right){}\mRightarrow{}  le[left;right];
intformeq(left,right){}\mRightarrow{}  eq[left;right];
intformand(left,right){}\mRightarrow{}  rec1,rec2.and[left;right;rec1;rec2];
intformor(left,right){}\mRightarrow{}  rec3,rec4.or[left;right;rec3;rec4];
intformimplies(left,right){}\mRightarrow{}  rec5,rec6.implies[left;right;rec5;rec6];
intformnot(form){}\mRightarrow{}  rec7.not[form;rec7])    \mmember{}  A)

By

Latex:
(ProveDatatypeIndWfSimple'  int\_formula\_ind\_wf)

Home Index