---

Step * 2 of Lemma mul_poly-sq


1. u : iMonomial()
2. v : iMonomial() List
3. ∀[q:iMonomial() List]. (mul_ipoly(v;q) ~ mul-ipoly(v;q))
⊢ ∀[q:iMonomial() List]. (mul_ipoly([u / v];q) ~ mul-ipoly([u / v];q))
BY
{ ((RepUR ``mul_ipoly mul-ipoly`` 0 THEN Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Reduce 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN DVar `q'
   THEN Reduce 0
   THEN Try (Trivial)) }

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

---

Latex:

---

Latex:

1.  u  :  iMonomial()
2.  v  :  iMonomial()  List
3.  \mforall{}[q:iMonomial()  List].  (mul\_ipoly(v;q)  \msim{}  mul-ipoly(v;q))
\mvdash{}  \mforall{}[q:iMonomial()  List].  (mul\_ipoly([u  /  v];q)  \msim{}  mul-ipoly([u  /  v];q))


By

---

Latex:
((RepUR  ``mul\_ipoly  mul-ipoly``  0  THEN  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  DVar  `q'
  THEN  Reduce  0
  THEN  Try  (Trivial))

---

Home Index