---

Step * of Lemma int_term_ind_wf

∀[A:Type]. ∀[R:A ⟶ int_term() ⟶ ℙ]. ∀[v:int_term()]. ∀[Constant:const:ℤ ⟶ {x:A| R[x;"const"]} ].
∀[Var:var:ℤ ⟶ {x:A| R[x;vvar]} ]. ∀[Add:left:int_term()
                                        ⟶ right:int_term()
                                        ⟶ {x:A| R[x;left]} 
                                        ⟶ {x:A| R[x;right]} 
                                        ⟶ {x:A| R[x;left (+) right]} ]. ∀[Subtract:left:int_term()
                                                                                   ⟶ right:int_term()
                                                                                   ⟶ {x:A| R[x;left]} 
                                                                                   ⟶ {x:A| R[x;right]} 
                                                                                   ⟶ {x:A| R[x;left (-) right]} ].
∀[Multiply:left:int_term() ⟶ right:int_term() ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left (*) right]} \000C].
∀[Minus:num:int_term() ⟶ {x:A| R[x;num]}  ⟶ {x:A| R[x;"-"num]} ].
  (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])  ∈ {x:A| R[x;v]} )
BY
{ (ProveDatatypeIndWfByLemma int_term-definition) }

---

Latex:

---

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


By

---

Latex:
(ProveDatatypeIndWfByLemma  int\_term-definition)

---

Home Index