---

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


1. r : CRng
2. u : iMonomial()
3. v : iMonomial() List
4. ∀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))
5. p : iMonomial() List
6. 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:
                    add-ipoly(p;mul-mono-poly(u;q)))) ≡ ipolynomial-term(p)
(+) (ipolynomial-term([u / v]) (*) ipolynomial-term(q))
BY
{ ((InstLemma `mul-mono-poly-ringeq` [⌜r⌝]⋅ THENA Auto)
   THEN (InstLemma `ipolynomial-term-cons-ringeq` [⌜r⌝]⋅ THENA Auto)
   THEN (InstLemma `add-ipoly-ringeq` [⌜r⌝]⋅ THENA Auto)
   THEN RWW "4 -3 -2 -1" 0
   THEN Auto
   THEN GenConclTerms Auto [⌜ipolynomial-term(p)⌝;⌜imonomial-term(u)⌝;
                            ⌜ipolynomial-term(v)⌝;⌜ipolynomial-term(q)⌝]⋅
   THEN All Thin) }

1
1. r : CRng
2. v1 : int_term()
3. v2 : int_term()
4. v3 : int_term()
5. v4 : int_term()
⊢ (v1 (+) (v2 (*) v4)) (+) (v3 (*) v4) ≡ v1 (+) ((v2 (+) v3) (*) v4)

---

Latex:

---

Latex:

1.  r  :  CRng
2.  u  :  iMonomial()
3.  v  :  iMonomial()  List
4.  \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))
5.  p  :  iMonomial()  List
6.  q  :  iMonomial()  List
\mvdash{}  ipolynomial-term(accumulate  (with  value  sofar  and  list  item  m):
                                        add-ipoly(sofar;mul-mono-poly(m;q))
                                      over  list:
                                          v
                                      with  starting  value:
                                        add-ipoly(p;mul-mono-poly(u;q))))  \mequiv{}  ipolynomial-term(p)
(+)  (ipolynomial-term([u  /  v])  (*)  ipolynomial-term(q))


By

---

Latex:
((InstLemma  `mul-mono-poly-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `ipolynomial-term-cons-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `add-ipoly-ringeq`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWW  "4  -3  -2  -1"  0
  THEN  Auto
  THEN  GenConclTerms  Auto  [\mkleeneopen{}ipolynomial-term(p)\mkleeneclose{};\mkleeneopen{}imonomial-term(u)\mkleeneclose{};
                                                    \mkleeneopen{}ipolynomial-term(v)\mkleeneclose{};\mkleeneopen{}ipolynomial-term(q)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index