---

Step * 2 2 1 of Lemma mul-ipoly-ringeq


1. r : CRng
2. u : iMonomial()
3. v : iMonomial() List
4. q : iMonomial() List
5. ∀[m:iMonomial()]. ∀[p:iMonomial() List].  ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)
6. (imonomial-term(u) (+) ipolynomial-term(v)) (*) ipolynomial-term(q) ≡ (imonomial-term(u) (*) ipolynomial-term(q))
(+) (ipolynomial-term(v) (*) ipolynomial-term(q))
⊢ ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));mul-mono-poly(u;q);v)) ≡ (imonomial-term(u)
(+) ipolynomial-term(v))
(*) ipolynomial-term(q)
BY
{ ((RWO "-1" 0 THENA Auto) THEN RepeatFor 2 (Thin (-1)) THEN MoveToConcl (-1) THEN MoveToConcl (-2)) }

1
1. r : CRng
2. v : iMonomial() List
⊢ ∀u:iMonomial(). ∀q:iMonomial() List.
    ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));mul-mono-poly(u;q);v)) ≡ (imonomial-term(u)
    (*) ipolynomial-term(q))
    (+) (ipolynomial-term(v) (*) ipolynomial-term(q))

---

Latex:

---

Latex:

1.  r  :  CRng
2.  u  :  iMonomial()
3.  v  :  iMonomial()  List
4.  q  :  iMonomial()  List
5.  \mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
          ipolynomial-term([m  /  p])  \mequiv{}  imonomial-term(m)  (+)  ipolynomial-term(p)
6.  (imonomial-term(u)  (+)  ipolynomial-term(v))  (*)  ipolynomial-term(q)  \mequiv{}  (imonomial-term(u)
(*)  ipolynomial-term(q))
(+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))
\mvdash{}  ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));mul-mono-poly(u;q);v)) 
\mequiv{}  (imonomial-term(u)  (+)  ipolynomial-term(v))  (*)  ipolynomial-term(q)


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)  THEN  RepeatFor  2  (Thin  (-1))  THEN  MoveToConcl  (-1)  THEN  MoveToConcl  (-2))

---

Home Index