---

Step * 2 of Lemma mul-mono-poly-req

.....aux..... 
1. m : iMonomial()
2. u : iMonomial()
3. v : iMonomial() List
4. ipolynomial-term(mul-mono-poly(m;v)) ≡ imonomial-term(m) (*) ipolynomial-term(v)
⊢ (mul-mono-poly(m;v))↓
BY
{ (GenConcl ⌜mul-mono-poly(m;v) = L ∈ (iMonomial() List)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  m  :  iMonomial()
2.  u  :  iMonomial()
3.  v  :  iMonomial()  List
4.  ipolynomial-term(mul-mono-poly(m;v))  \mequiv{}  imonomial-term(m)  (*)  ipolynomial-term(v)
\mvdash{}  (mul-mono-poly(m;v))\mdownarrow{}


By

---

Latex:
(GenConcl  \mkleeneopen{}mul-mono-poly(m;v)  =  L\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index