---

Step * 2 2 of Lemma mul-ipoly-ringeq


1. r : CRng
2. u : iMonomial()
3. v : iMonomial() List
4. q : iMonomial() List
5. ¬(q = [] ∈ (iMonomial() List))
⊢ ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));mul-mono-poly(u;q);v)) 
≡ ipolynomial-term([u / v]) (*) ipolynomial-term(q)
BY
{ (Thin (-1)
   THEN (InstLemma `ipolynomial-term-cons-ringeq` [⌜r⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (Assert ⌜(imonomial-term(u) (+) ipolynomial-term(v)) (*) ipolynomial-term(q) ≡ (imonomial-term(u)
                 (*) ipolynomial-term(q))
                 (+) (ipolynomial-term(v) (*) ipolynomial-term(q))⌝⋅
         THENA (GenConclTerms Auto [⌜imonomial-term(u)⌝;
                                         ⌜ipolynomial-term(v)⌝;⌜ipolynomial-term(q)⌝]⋅
                THEN All Thin
                THEN D 0
                THEN Reduce 0
                THEN Auto)
         )) }

1
1. r : CRng
2. u : iMonomial()
3. v : iMonomial() List
4. q : iMonomial() List
5. ∀[m:iMonomial()]. ∀[p:iMonomial() List].  ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)
6. (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.  r  :  CRng
2.  u  :  iMonomial()
3.  v  :  iMonomial()  List
4.  q  :  iMonomial()  List
5.  \mneg{}(q  =  [])
\mvdash{}  ipolynomial-term(eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;q));mul-mono-poly(u;q);v)) 
\mequiv{}  ipolynomial-term([u  /  v])  (*)  ipolynomial-term(q)


By

---

Latex:
(Thin  (-1)
  THEN  (InstLemma  `ipolynomial-term-cons-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (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{}
              THENA  (GenConclTerms  Auto  [\mkleeneopen{}imonomial-term(u)\mkleeneclose{};
                                                                              \mkleeneopen{}ipolynomial-term(v)\mkleeneclose{};\mkleeneopen{}ipolynomial-term(q)\mkleeneclose{}]\mcdot{}
                            THEN  All  Thin
                            THEN  D  0
                            THEN  Reduce  0
                            THEN  Auto)
              ))

---

Home Index