---

Step * 1 2 2 2 1 of Lemma minus-poly-equiv


1. u : iMonomial()
2. v : iMonomial() List
3. ∀i:ℕ||[u / v]||. ∀j:ℕi.  imonomial-less([u / v][j];[u / v][i])
4. ∀i:ℕ||v||. ∀j:ℕi.  imonomial-less(v[j];v[i])
5. ipolynomial-term(minus-poly(v)) ≡ "-"ipolynomial-term(v)
⊢ imonomial-term(minus-monomial(u)) (+) "-"ipolynomial-term(v) ≡ "-"imonomial-term(u) (+) ipolynomial-term(v)
BY
{ (DVar `u' THEN RepUR ``minus-monomial`` 0 THEN D 0 THEN Auto) }

1
1. u1 : ℤ-o
2. u2 : {vs:ℤ List| sorted(vs)} 
3. v : iMonomial() List
4. ∀i:ℕ||[<u1, u2> / v]||. ∀j:ℕi.  imonomial-less([<u1, u2> / v][j];[<u1, u2> / v][i])
5. ∀i:ℕ||v||. ∀j:ℕi.  imonomial-less(v[j];v[i])
6. ipolynomial-term(minus-poly(v)) ≡ "-"ipolynomial-term(v)
7. f : ℤ ⟶ ℤ
⊢ int_term_value(f;imonomial-term(<-u1, u2>) (+) "-"ipolynomial-term(v)) = int_term_value(f;"-"imonomial-term(<u1, u2>) \000C(+) ipolynomial-term(v)) ∈ ℤ

---

Latex:

---

Latex:

1.  u  :  iMonomial()
2.  v  :  iMonomial()  List
3.  \mforall{}i:\mBbbN{}||[u  /  v]||.  \mforall{}j:\mBbbN{}i.    imonomial-less([u  /  v][j];[u  /  v][i])
4.  \mforall{}i:\mBbbN{}||v||.  \mforall{}j:\mBbbN{}i.    imonomial-less(v[j];v[i])
5.  ipolynomial-term(minus-poly(v))  \mequiv{}  "-"ipolynomial-term(v)
\mvdash{}  imonomial-term(minus-monomial(u))  (+)  "-"ipolynomial-term(v)  \mequiv{}  "-"imonomial-term(u)
    (+)  ipolynomial-term(v)


By

---

Latex:
(DVar  `u'  THEN  RepUR  ``minus-monomial``  0  THEN  D  0  THEN  Auto)

---

Home Index