---

Step * 2 1 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))
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)
BY
{ ((InstLemma `cbv_list_accum-is-list_accum` [⌜iMonomial()⌝;⌜iMonomial() List⌝;⌜v⌝;⌜mul-mono-poly(u;[u1 / v1])⌝]⋅
    THENA Auto
    )
   THEN (RWO "-1" 0 THENA Auto)
   ) }

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
6. ∀p,q:iMonomial() List.  (add_ipoly(p;q) ∈ iMonomial() List)
7. ∀[f:(iMonomial() List) ⟶ iMonomial() ⟶ (iMonomial() List)]
     cbv_list_accum(x,a.f[x;a];mul-mono-poly(u;[u1 / v1]);v) ~ accumulate (with value x and list item a):
                                                                f[x;a]
                                                               over list:
                                                                 v
                                                               with starting value:
                                                                mul-mono-poly(u;[u1 / v1])) 
     supposing value-type(iMonomial() List)
⊢ value-type(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)
7. ∀[f:(iMonomial() List) ⟶ iMonomial() ⟶ (iMonomial() List)]
     cbv_list_accum(x,a.f[x;a];mul-mono-poly(u;[u1 / v1]);v) ~ accumulate (with value x and list item a):
                                                                f[x;a]
                                                               over list:
                                                                 v
                                                               with starting value:
                                                                mul-mono-poly(u;[u1 / v1])) 
     supposing value-type(iMonomial() List)
⊢ accumulate (with value sofar and list item m):
   add_ipoly(sofar;mul-mono-poly(m;[u1 / v1]))
  over list:
    v
  with starting value:
   mul-mono-poly(u;[u1 / v1])) ~ 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
6.  \mforall{}p,q:iMonomial()  List.    (add\_ipoly(p;q)  \mmember{}  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:
((InstLemma  `cbv\_list\_accum-is-list\_accum`  [\mkleeneopen{}iMonomial()\mkleeneclose{};\mkleeneopen{}iMonomial()  List\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};
    \mkleeneopen{}mul-mono-poly(u;[u1  /  v1])\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (RWO  "-1"  0  THENA  Auto)
  )

---

Home Index