---

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


1. v : iMonomial() List
2. ∀p,q:iMonomial() List.
     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))
3. u : iMonomial()
4. q : iMonomial() List
⊢ ipolynomial-term(mul-mono-poly(u;q)) (+) (ipolynomial-term(v) (*) ipolynomial-term(q)) ≡ (imonomial-term(u)
  (*) ipolynomial-term(q))
  (+) (ipolynomial-term(v) (*) ipolynomial-term(q))
BY
{ (RWW "mul-mono-poly-equiv" 0 THEN Auto) }

1
1. v : iMonomial() List
2. ∀p,q:iMonomial() List.
     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))
3. u : iMonomial()
4. q : iMonomial() List
⊢ (imonomial-term(u) (*) ipolynomial-term(q)) (+) (ipolynomial-term(v) (*) ipolynomial-term(q)) ≡ (imonomial-term(u)
  (*) ipolynomial-term(q))
  (+) (ipolynomial-term(v) (*) ipolynomial-term(q))

---

Latex:

---

Latex:

1.  v  :  iMonomial()  List
2.  \mforall{}p,q:iMonomial()  List.
          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))
3.  u  :  iMonomial()
4.  q  :  iMonomial()  List
\mvdash{}  ipolynomial-term(mul-mono-poly(u;q))  (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q)) 
    \mequiv{}  (imonomial-term(u)  (*)  ipolynomial-term(q))  (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))


By

---

Latex:
(RWW  "mul-mono-poly-equiv"  0  THEN  Auto)

---

Home Index