---

Step * of Lemma rat_term_ind_wf

∀[A:Type]. ∀[R:A ⟶ rat_term() ⟶ ℙ]. ∀[v:rat_term()]. ∀[Constant:const:ℤ ⟶ {x:A| R[x;"const"]} ].
∀[Var:var:ℤ ⟶ {x:A| R[x;rtermVar(var)]} ]. ∀[Add:left:rat_term()
                                                 ⟶ right:rat_term()
                                                 ⟶ {x:A| R[x;left]} 
                                                 ⟶ {x:A| R[x;right]} 
                                                 ⟶ {x:A| R[x;left "+" right]} ]. ∀[Subtract:left:rat_term()
                                                                                            ⟶ right:rat_term()
                                                                                            ⟶ {x:A| R[x;left]} 
                                                                                            ⟶ {x:A| R[x;right]} 
                                                                                            ⟶ {x:A| 
                                                                                                R[x;left "-" right]} ].
∀[Multiply:left:rat_term() ⟶ right:rat_term() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left "*" right]} \000C].
∀[Divide:num:rat_term() ⟶ denom:rat_term() ⟶ {x:A| R[x;num]}  ⟶ {x:A| R[x;denom]}  ⟶ {x:A| R[x;num "/" denom]} ].
∀[Minus:num:rat_term() ⟶ {x:A| R[x;num]}  ⟶ {x:A| R[x;rtermMinus(num)]} ].
  (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])  ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{rat_term-definition:o, 1:l, i:l}⋅ }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  rat\_term()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:rat\_term()].  \mforall{}[Constant:const:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;"const"]\}  ].
\mforall{}[Var:var:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;rtermVar(var)]\}  ].  \mforall{}[Add:left:rat\_term()
                                                                                                  {}\mrightarrow{}  right:rat\_term()
                                                                                                  {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                                  {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                                  {}\mrightarrow{}  \{x:A|  R[x;left  "+"  right]\}  ].
\mforall{}[Subtract:left:rat\_term()
                      {}\mrightarrow{}  right:rat\_term()
                      {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                      {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                      {}\mrightarrow{}  \{x:A|  R[x;left  "-"  right]\}  ].  \mforall{}[Multiply:left:rat\_term()
                                                                                                            {}\mrightarrow{}  right:rat\_term()
                                                                                                            {}\mrightarrow{}  \{x:A|  R[x;left]\} 
                                                                                                            {}\mrightarrow{}  \{x:A|  R[x;right]\} 
                                                                                                            {}\mrightarrow{}  \{x:A|  R[x;left  "*"  right]\}  ].
\mforall{}[Divide:num:rat\_term()
                  {}\mrightarrow{}  denom:rat\_term()
                  {}\mrightarrow{}  \{x:A|  R[x;num]\} 
                  {}\mrightarrow{}  \{x:A|  R[x;denom]\} 
                  {}\mrightarrow{}  \{x:A|  R[x;num  "/"  denom]\}  ].  \mforall{}[Minus:num:rat\_term()
                                                                                                {}\mrightarrow{}  \{x:A|  R[x;num]\} 
                                                                                                {}\mrightarrow{}  \{x:A|  R[x;rtermMinus(num)]\}  ].
    (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{}  \{x:A|  R[x;v]\}  )


By

---

Latex:
ProveDatatypeIndWf  TERMOF\{rat\_term-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index