---

Step * 2 of Lemma imonomial-cons


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]>)) ∈ ℤ)
BY
{ Auto }

1
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) ∈ ℤ)
4. u@0 : ℤ
5. a : ℤ
6. f : ℤ ⟶ ℤ
⊢ int_term_value(f;imonomial-term(<a, [u@0; [u / v]]>)) = int_term_value(f;imonomial-term(<a * (f u@0), [u / v]>)) ∈ ℤ

---

Latex:

---

Latex:

1.  u  :  \mBbbZ{}
2.  v  :  \mBbbZ{}  List
3.  \mforall{}u,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.    (int\_term\_value(f;imonomial-term(<a,  [u  /  v]>))  =  int\_term\_value(f;imonomial-\000Cterm(<a  *  (f  u),  v>)))
\mvdash{}  \mforall{}u@0,a:\mBbbZ{}.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbZ{}.
        (int\_term\_value(f;imonomial-term(<a,  [u@0;  [u  /  v]]>))  =  int\_term\_value(f;imonomial-term(<a  *  (f\000C  u@0),  [u  /  v]>)))


By

---

Latex:
Auto

---

Home Index