---

Step * 2 1 of Lemma mul_poly-sq


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
⊢ cbv_list_accum(sofar,m.add_ipoly(sofar;mul-mono-poly(m;[u1 / v1]));mul-mono-poly(u;[u1 / v1]);v) 
~ eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;[u1 / v1]));mul-mono-poly(u;[u1 / v1]);v)
BY
{ Assert ⌜∀p,q:iMonomial() List.  (add_ipoly(p;q) ∈ iMonomial() List)⌝⋅ }

1
.....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)

2
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
6. ∀p,q:iMonomial() List.  (add_ipoly(p;q) ∈ iMonomial() List)
⊢ cbv_list_accum(sofar,m.add_ipoly(sofar;mul-mono-poly(m;[u1 / v1]));mul-mono-poly(u;[u1 / v1]);v) 
~ eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;[u1 / v1]));mul-mono-poly(u;[u1 / v1]);v)

---

Latex:

---

Latex:

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{}  cbv\_list\_accum(sofar,m.add\_ipoly(sofar;mul-mono-poly(m;[u1  /  v1]));mul-mono-poly(u;[u1  /  v1]);v) 
\msim{}  eager-accum(sofar,m.add-ipoly(sofar;mul-mono-poly(m;[u1  /  v1]));mul-mono-poly(u;[u1  /  v1]);v)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}p,q:iMonomial()  List.    (add\_ipoly(p;q)  \mmember{}  iMonomial()  List)\mkleeneclose{}\mcdot{}

---

Home Index