---

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


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(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));p;v)) ≡ ipolynomial-term(p)
              (+) (ipolynomial-term(v) (*) ipolynomial-term(q))⌝⋅
   THENM (Auto THEN RWW "2 mul-mono-poly-req" 0 THEN Auto THEN RelRST THEN Auto)
   )
   THEN 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))
⊢ ∀p,q:iMonomial() List.
    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))

---

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(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));p;v)) 
                        \mequiv{}  ipolynomial-term(p)  (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  RWW  "2  mul-mono-poly-req"  0  THEN  Auto  THEN  RelRST  THEN  Auto)
  )
  THEN  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