---

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


1. u : iMonomial()
2. v : iMonomial() List
3. 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(v))
  (*) ipolynomial-term(q)
BY
{ Assert ⌜(imonomial-term(u) (+) ipolynomial-term(v)) (*) ipolynomial-term(q) ≡ (imonomial-term(u)
          (*) ipolynomial-term(q))
          (+) (ipolynomial-term(v) (*) ipolynomial-term(q))⌝⋅ }

1
.....assertion..... 
1. u : iMonomial()
2. v : iMonomial() List
3. q : iMonomial() List
⊢ (imonomial-term(u) (+) ipolynomial-term(v)) (*) ipolynomial-term(q) ≡ (imonomial-term(u) (*) ipolynomial-term(q))
  (+) (ipolynomial-term(v) (*) ipolynomial-term(q))

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  \mkleeneopen{}(imonomial-term(u)  (+)  ipolynomial-term(v))  (*)  ipolynomial-term(q)  \mequiv{}  (imonomial-term(u)
                (*)  ipolynomial-term(q))
                (+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))\mkleeneclose{}\mcdot{}

---

Home Index