---

Step * of Lemma imonomial-cons

∀v:ℤ List. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u / v]>)) = int_term_value(f;imonomial-term(<a * (f\000C u), v>)) ∈ ℤ)
BY
{ InductionOnList }

1
∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u]>)) = int_term_value(f;imonomial-term(<a * (f u), []>)) ∈ ℤ)

2
1. u : ℤ
2. v : ℤ List
3. ∀u,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u / v]>)) = int_term_value(f;imonomial-term(<a * (f u), v>)\000C) ∈ ℤ)
⊢ ∀u@0,a:ℤ. ∀f:ℤ ⟶ ℤ.  (int_term_value(f;imonomial-term(<a, [u@0; [u / v]]>)) = int_term_value(f;imonomial-term(<a * (f\000C u@0), [u / v]>)) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}v:\mBbbZ{}  List.  \mforall{}u,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.    (int\_term\_value(f;imonomial-term(<a,  [u  /  v]>))  =  int\_term\_value(f;im\000Conomial-term(<a  *  (f  u),  v>)))


By

---

Latex:
InductionOnList

---

Home Index