---

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


1. r : CRng
2. v : iMonomial() List
3. p : iMonomial() List
4. q : iMonomial() List
5. ipolynomial-term(accumulate (with value sofar and list item m):
                     add-ipoly(sofar;mul-mono-poly(m;q))
                    over list:
                      v
                    with starting value:
                     p)) ≡ ipolynomial-term(p) (+) (ipolynomial-term(v) (*) ipolynomial-term(q))
⊢ ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));p;v)) ≡ ipolynomial-term(p)
(+) (ipolynomial-term(v) (*) ipolynomial-term(q))
BY
{ ((InstLemma `eager-accum-list_accum` [⌜iMonomial()⌝;⌜iMonomial() List⌝]⋅ THENA Auto) THEN RWO  "-1" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  v  :  iMonomial()  List
3.  p  :  iMonomial()  List
4.  q  :  iMonomial()  List
5.  ipolynomial-term(accumulate  (with  value  sofar  and  list  item  m):
                                          add-ipoly(sofar;mul-mono-poly(m;q))
                                        over  list:
                                            v
                                        with  starting  value:
                                          p))  \mequiv{}  ipolynomial-term(p)  (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))
\mvdash{}  ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));p;v)) 
\mequiv{}  ipolynomial-term(p)  (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))


By

---

Latex:
((InstLemma  `eager-accum-list\_accum`  [\mkleeneopen{}iMonomial()\mkleeneclose{};\mkleeneopen{}iMonomial()  List\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index