---

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