---

Step * 1 2 of Lemma fps-summation-coeff


1. X : Type
2. r : CRng
3. T : Type
4. f : T ⟶ PowerSeries(X;r)
5. m : bag(X)
6. b : T List
7. ¬↑null(b)
8. ||b|| ≥ 1 
9. (accumulate (with value c and list item x):
     λb.(+r (f[x] b) (c b))
    over list:
      firstn(||b|| - 1;b)
    with starting value:
     λb.0) 
    m)
= accumulate (with value c and list item x):
   +r (f[x] m) c
  over list:
    firstn(||b|| - 1;b)
  with starting value:
   0)
∈ |r|
⊢ (accumulate (with value c and list item x):
    λb.(+r (f[x] b) (c b))
   over list:
     firstn(||b|| - 1;b) @ [last(b)]
   with starting value:
    λb.0) 
   m)
= accumulate (with value c and list item x):
   +r (f[x] m) c
  over list:
    firstn(||b|| - 1;b) @ [last(b)]
  with starting value:
   0)
∈ |r|
BY
{ ((RWO "list_accum_append" 0 THENA Auto) THEN Reduce 0 THEN EqCD THEN Auto THEN Fold `power-series` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  r  :  CRng
3.  T  :  Type
4.  f  :  T  {}\mrightarrow{}  PowerSeries(X;r)
5.  m  :  bag(X)
6.  b  :  T  List
7.  \mneg{}\muparrow{}null(b)
8.  ||b||  \mgeq{}  1 
9.  (accumulate  (with  value  c  and  list  item  x):
          \mlambda{}b.(+r  (f[x]  b)  (c  b))
        over  list:
            firstn(||b||  -  1;b)
        with  starting  value:
          \mlambda{}b.0) 
        m)
=  accumulate  (with  value  c  and  list  item  x):
      +r  (f[x]  m)  c
    over  list:
        firstn(||b||  -  1;b)
    with  starting  value:
      0)
\mvdash{}  (accumulate  (with  value  c  and  list  item  x):
        \mlambda{}b.(+r  (f[x]  b)  (c  b))
      over  list:
          firstn(||b||  -  1;b)  @  [last(b)]
      with  starting  value:
        \mlambda{}b.0) 
      m)
=  accumulate  (with  value  c  and  list  item  x):
      +r  (f[x]  m)  c
    over  list:
        firstn(||b||  -  1;b)  @  [last(b)]
    with  starting  value:
      0)


By

---

Latex:
((RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto
  THEN  Fold  `power-series`  0
  THEN  Auto)

---

Home Index