---

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

.....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))
BY
{ (GenConclTerms Auto [⌜imonomial-term(u)⌝;
                            ⌜ipolynomial-term(v)⌝;⌜ipolynomial-term(q)⌝]⋅
   THEN All Thin
   ) }

1
1. v1 : int_term()
2. v2 : int_term()
3. v3 : int_term()
⊢ (v1 (+) v2) (*) v3 ≡ (v1 (*) v3) (+) (v2 (*) v3)

---

Latex:

---

Latex:
.....assertion..... 
1.  u  :  iMonomial()
2.  v  :  iMonomial()  List
3.  q  :  iMonomial()  List
\mvdash{}  (imonomial-term(u)  (+)  ipolynomial-term(v))  (*)  ipolynomial-term(q)  \mequiv{}  (imonomial-term(u)
(*)  ipolynomial-term(q))
(+)  (ipolynomial-term(v)  (*)  ipolynomial-term(q))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}imonomial-term(u)\mkleeneclose{};
                                                    \mkleeneopen{}ipolynomial-term(v)\mkleeneclose{};\mkleeneopen{}ipolynomial-term(q)\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  )

---

Home Index