---

Step * 2 1 1 of Lemma mul_poly-sq

.....assertion..... 
1. u : iMonomial()
2. v : iMonomial() List
3. ∀[q:iMonomial() List]. (mul_ipoly(v;q) ~ mul-ipoly(v;q))
4. u1 : iMonomial()
5. v1 : iMonomial() List
⊢ ∀p,q:iMonomial() List.  (add_ipoly(p;q) ∈ iMonomial() List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
.....assertion..... 
1.  u  :  iMonomial()
2.  v  :  iMonomial()  List
3.  \mforall{}[q:iMonomial()  List].  (mul\_ipoly(v;q)  \msim{}  mul-ipoly(v;q))
4.  u1  :  iMonomial()
5.  v1  :  iMonomial()  List
\mvdash{}  \mforall{}p,q:iMonomial()  List.    (add\_ipoly(p;q)  \mmember{}  iMonomial()  List)


By

---

Latex:
ProveWfLemma

---

Home Index