---

Step * of Lemma rat_term_ind_wf_simple

∀[A:Type]. ∀[v:rat_term()]. ∀[Constant,Var:var:ℤ ⟶ A]. ∀[Add,Subtract,Multiply,Divide:num:rat_term()
                                                                                       ⟶ denom:rat_term()
                                                                                       ⟶ A
                                                                                       ⟶ A
                                                                                       ⟶ A]. ∀[Minus:num:rat_term()
                                                                                                      ⟶ A
                                                                                                      ⟶ A].
  (rat_term_ind(v;
                rtermConstant(const)⇒ Constant[const];
                rtermVar(var)⇒ Var[var];
                rtermAdd(left,right)⇒ rec1,rec2.Add[left;right;rec1;rec2];
                rtermSubtract(left,right)⇒ rec3,rec4.Subtract[left;right;rec3;rec4];
                rtermMultiply(left,right)⇒ rec5,rec6.Multiply[left;right;rec5;rec6];
                rtermDivide(num,denom)⇒ rec7,rec8.Divide[num;denom;rec7;rec8];
                rtermMinus(num)⇒ rec9.Minus[num;rec9])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 0 `rat_term_ind_wf` }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[v:rat\_term()].  \mforall{}[Constant,Var:var:\mBbbZ{}  {}\mrightarrow{}  A].
\mforall{}[Add,Subtract,Multiply,Divide:num:rat\_term()  {}\mrightarrow{}  denom:rat\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
\mforall{}[Minus:num:rat\_term()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (rat\_term\_ind(v;
                                rtermConstant(const){}\mRightarrow{}  Constant[const];
                                rtermVar(var){}\mRightarrow{}  Var[var];
                                rtermAdd(left,right){}\mRightarrow{}  rec1,rec2.Add[left;right;rec1;rec2];
                                rtermSubtract(left,right){}\mRightarrow{}  rec3,rec4.Subtract[left;right;rec3;rec4];
                                rtermMultiply(left,right){}\mRightarrow{}  rec5,rec6.Multiply[left;right;rec5;rec6];
                                rtermDivide(num,denom){}\mRightarrow{}  rec7,rec8.Divide[num;denom;rec7;rec8];
                                rtermMinus(num){}\mRightarrow{}  rec9.Minus[num;rec9])    \mmember{}  A)


By

---

Latex:
ProveDatatypeIndWfSimple  0  `rat\_term\_ind\_wf`

---

Home Index