---

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


1. r : CRng
2. 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 (InstLemma `mul-mono-poly-ringeq` [⌜r⌝]⋅ THENA Auto)
          THEN RWW "3 -1" 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. r : CRng
2. 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. r : CRng
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))
⊢ ∀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.  r  :  CRng
2.  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  (InstLemma  `mul-mono-poly-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  RWW  "3  -1"  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