---

Step * of Lemma int_formula_ind_wf

∀[A:Type]. ∀[R:A ⟶ int_formula() ⟶ ℙ]. ∀[v:int_formula()]. ∀[less:left:int_term()
                                                                    ⟶ right:int_term()
                                                                    ⟶ {x:A| R[x;(left "<" right)]} ].
∀[le:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left "≤" right]} ]. ∀[eq:left:int_term()
                                                                              ⟶ right:int_term()
                                                                              ⟶ {x:A| R[x;left "=" right]} ].
∀[and:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left "∧" right]}\000C ].
∀[or:left:int_formula() ⟶ right:int_formula() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left "or" right]}\000C ].
∀[implies:left:int_formula()
          ⟶ right:int_formula()
          ⟶ {x:A| R[x;left]} 
          ⟶ {x:A| R[x;right]} 
          ⟶ {x:A| R[x;left "=>" right]} ]. ∀[not:form:int_formula() ⟶ {x:A| R[x;form]}  ⟶ {x:A| R[x;"¬"form]} ].
  (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])  ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma⋅ int_formula-definition) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  int\_formula()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:int\_formula()].  \mforall{}[less:left:int\_term()
                                                                                                                                        {}\mrightarrow{}  right:int\_term()
                                                                                                                                        {}\mrightarrow{}  \{x:A| 
                                                                                                                                                R[x;(left  "<"  right)]\}  ].
\mforall{}[le:left:int\_term()  {}\mrightarrow{}  right:int\_term()  {}\mrightarrow{}  \{x:A|  R[x;left  "\mleq{}"  right]\}  ].
\mforall{}[eq:left:int\_term()  {}\mrightarrow{}  right:int\_term()  {}\mrightarrow{}  \{x:A|  R[x;left  "="  right]\}  ].
\mforall{}[and:left:int\_formula()
            {}\mrightarrow{}  right:int\_formula()
            {}\mrightarrow{}  \{x:A|  R[x;left]\} 
            {}\mrightarrow{}  \{x:A|  R[x;right]\} 
            {}\mrightarrow{}  \{x:A|  R[x;left  "\mwedge{}"  right]\}  ].  \mforall{}[or:left:int\_formula()
                                                                                      {}\mrightarrow{}  right:int\_formula()
                                                                                      {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                      {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                      {}\mrightarrow{}  \{x:A|  R[x;left  "or"  right]\}  ].
\mforall{}[implies:left:int\_formula()
                    {}\mrightarrow{}  right:int\_formula()
                    {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                    {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                    {}\mrightarrow{}  \{x:A|  R[x;left  "=>"  right]\}  ].  \mforall{}[not:form:int\_formula()
                                                                                                  {}\mrightarrow{}  \{x:A|  R[x;form]\} 
                                                                                                  {}\mrightarrow{}  \{x:A|  R[x;"\mneg{}"form]\}  ].
    (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{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
(ProveDatatypeIndWfByLemma\mcdot{}  int\_formula-definition)

---

Home Index