---

Step * of Lemma int_term_ind_wf_simple

∀[A:Type]. ∀[v:int_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply:left:int_term()
                                                                                ⟶ right:int_term()
                                                                                ⟶ A
                                                                                ⟶ A
                                                                                ⟶ A].
∀[Minus:num:int_term() ⟶ A ⟶ A].
  (int_term_ind(v;
                itermConstant(const)⇒ Constant[const];
                itermVar(var)⇒ Var[var];
                itermAdd(left,right)⇒ rec1,rec2.Add[left;right;rec1;rec2];
                itermSubtract(left,right)⇒ rec3,rec4.Subtract[left;right;rec3;rec4];
                itermMultiply(left,right)⇒ rec5,rec6.Multiply[left;right;rec5;rec6];
                itermMinus(num)⇒ rec7.Minus[num;rec7])  ∈ A)
BY
{ (ProveDatatypeIndWfSimple' int_term_ind_wf) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[v:int\_term()].  \mforall{}[Constant,Var:var:\mBbbZ{}  {}\mrightarrow{}  A].  \mforall{}[Add,Subtract,Multiply:left:int\_term()
                                                                                                                                                                {}\mrightarrow{}  right:int\_term()
                                                                                                                                                                {}\mrightarrow{}  A
                                                                                                                                                                {}\mrightarrow{}  A
                                                                                                                                                                {}\mrightarrow{}  A].
\mforall{}[Minus:num:int\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (int\_term\_ind(v;
                                itermConstant(const){}\mRightarrow{}  Constant[const];
                                itermVar(var){}\mRightarrow{}  Var[var];
                                itermAdd(left,right){}\mRightarrow{}  rec1,rec2.Add[left;right;rec1;rec2];
                                itermSubtract(left,right){}\mRightarrow{}  rec3,rec4.Subtract[left;right;rec3;rec4];
                                itermMultiply(left,right){}\mRightarrow{}  rec5,rec6.Multiply[left;right;rec5;rec6];
                                itermMinus(num){}\mRightarrow{}  rec7.Minus[num;rec7])    \mmember{}  A)


By

---

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

---

Home Index