---

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

.....assertion..... 
1. v : iMonomial() List
⊢ ∀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))
BY
{ ((ListInd 1 THEN Auto) THEN Reduce 0) }

1
1. p : iMonomial() List
2. q : iMonomial() List
⊢ ipolynomial-term(p) ≡ ipolynomial-term(p) (+) (ipolynomial-term([]) (*) ipolynomial-term(q))

2
1. u : iMonomial()
2. v : iMonomial() List
3. ∀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))
4. p : iMonomial() List
5. 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:
                    add-ipoly(p;mul-mono-poly(u;q)))) ≡ ipolynomial-term(p)
(+) (ipolynomial-term([u / v]) (*) ipolynomial-term(q))

---

Latex:

---

Latex:
.....assertion..... 
1.  v  :  iMonomial()  List
\mvdash{}  \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))


By

---

Latex:
((ListInd  1  THEN  Auto)  THEN  Reduce  0)

---

Home Index