---

Step * 1 1 1 1 of Lemma mul-monomials-equiv


1. bs : ℤ List
2. f : ℤ ⟶ ℤ
⊢ ∀as:ℤ List. (int_term_value(f;imonomial-term(<1, merge-int(as;bs)>)) = (int_term_value(f;imonomial-term(<1, as>)) * in\000Ct_term_value(f;imonomial-term(<1, bs>))) ∈ ℤ)
BY
{ ListInd 1 }

1
1. f : ℤ ⟶ ℤ
⊢ ∀as:ℤ List. (int_term_value(f;imonomial-term(<1, merge-int(as;[])>)) = (int_term_value(f;imonomial-term(<1, as>)) * in\000Ct_term_value(f;imonomial-term(<1, []>))) ∈ ℤ)

2
1. f : ℤ ⟶ ℤ
2. u : ℤ
3. v : ℤ List
4. ∀as:ℤ List. (int_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (int_term_value(f;imonomial-term(<1, as>)) * in\000Ct_term_value(f;imonomial-term(<1, v>))) ∈ ℤ)
⊢ ∀as:ℤ List. (int_term_value(f;imonomial-term(<1, merge-int(as;[u / v])>)) = (int_term_value(f;imonomial-term(<1, as>))\000C * int_term_value(f;imonomial-term(<1, [u / v]>))) ∈ ℤ)

---

Latex:

---

Latex:

1.  bs  :  \mBbbZ{}  List
2.  f  :  \mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}
\mvdash{}  \mforall{}as:\mBbbZ{}  List.  (int\_term\_value(f;imonomial-term(ə,  merge-int(as;bs)>))  =  (int\_term\_value(f;imonomial\000C-term(ə,  as>))  *  int\_term\_value(f;imonomial-term(ə,  bs>))))


By

---

Latex:
ListInd  1

---

Home Index