---

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


1. 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))
BY
{ Assert ⌜∀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))⌝⋅ }

1
.....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))

2
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))
⊢ ∀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.  v  :  iMonomial()  List
\mvdash{}  \mforall{}u:iMonomial().  \mforall{}q:iMonomial()  List.
        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(q))  (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))


By

---

Latex:
Assert  \mkleeneopen{}\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))\mkleeneclose{}\mcdot{}

---

Home Index