---

Step * of Lemma imonomial-term-linear

∀f:ℤ ⟶ ℤ. ∀ws:ℤ List. ∀c:ℤ.  (int_term_value(f;imonomial-term(<c, ws>)) = (c * int_term_value(f;imonomial-term(<1, ws>)\000C)) ∈ ℤ)
BY
{ InductionOnList }

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

2
1. f : ℤ ⟶ ℤ
2. u : ℤ
3. v : ℤ List
4. ∀c:ℤ. (int_term_value(f;imonomial-term(<c, v>)) = (c * int_term_value(f;imonomial-term(<1, v>))) ∈ ℤ)
⊢ ∀c:ℤ. (int_term_value(f;imonomial-term(<c, [u / v]>)) = (c * int_term_value(f;imonomial-term(<1, [u / v]>))) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}ws:\mBbbZ{}  List.  \mforall{}c:\mBbbZ{}.    (int\_term\_value(f;imonomial-term(<c,  ws>))  =  (c  *  int\_term\_value(f;imo\000Cnomial-term(ə,  ws>))))


By

---

Latex:
InductionOnList

---

Home Index