---

Step * 1 1 of Lemma bag-summation-append


1. R : Type
2. add : R ⟶ R ⟶ R
3. zero : R
4. IsMonoid(R;add;zero)
5. Comm(R;add)
6. T : Type
7. f : T ⟶ R
8. L : T List
9. ¬↑null(L)
10. ||L|| ≥ 1 
11. ∀c:bag(T). (Σ(x∈firstn(||L|| - 1;L) + c). f[x] = (Σ(x∈firstn(||L|| - 1;L)). f[x] add Σ(x∈c). f[x]) ∈ R)
12. c : bag(T)
13. Σ(x∈firstn(||L|| - 1;L)). f[x] ∈ R
14. v : R
⊢ (v add Σ(x∈{last(L)} + c). f[x]) = ((v add Σ(x∈{last(L)}). f[x]) add Σ(x∈c). f[x]) ∈ R
BY
{ (D 4
   THEN DupHyp 4
   THEN Unfold `assoc` -1
   THEN (RWO "-1<" 0 THENM EqCD)
   THEN Auto
   THEN RepUR ``bag-append bag-summation bag-accum`` 0
   THEN (RWO "list_accum_append" 0 THENA Auto)
   THEN RepUR ``single-bag`` 0
   THEN GenConclAtAddr [2;2]) }

1
1. R : Type
2. add : R ⟶ R ⟶ R
3. zero : R
4. Assoc(R;add)
5. Ident(R;add;zero)
6. Comm(R;add)
7. T : Type
8. f : T ⟶ R
9. L : T List
10. ¬↑null(L)
11. ||L|| ≥ 1 
12. ∀c:bag(T). (Σ(x∈firstn(||L|| - 1;L) + c). f[x] = (Σ(x∈firstn(||L|| - 1;L)). f[x] add Σ(x∈c). f[x]) ∈ R)
13. c : bag(T)
14. Σ(x∈firstn(||L|| - 1;L)). f[x] ∈ R
15. v : R
16. ∀[x,y,z:R].  ((x add (y add z)) = ((x add y) add z) ∈ R)
17. v1 : R
18. (add f[last(L)] zero) = v1 ∈ R
⊢ accumulate (with value c and list item x):
   add f[x] c
  over list:
    c
  with starting value:
   v1)
= (v1 add accumulate (with value c and list item x): add f[x] cover list:  cwith starting value: zero))
∈ R

---

Latex:

---

Latex:

1.  R  :  Type
2.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
3.  zero  :  R
4.  IsMonoid(R;add;zero)
5.  Comm(R;add)
6.  T  :  Type
7.  f  :  T  {}\mrightarrow{}  R
8.  L  :  T  List
9.  \mneg{}\muparrow{}null(L)
10.  ||L||  \mgeq{}  1 
11.  \mforall{}c:bag(T)
            (\mSigma{}(x\mmember{}firstn(||L||  -  1;L)  +  c).  f[x]  =  (\mSigma{}(x\mmember{}firstn(||L||  -  1;L)).  f[x]  add  \mSigma{}(x\mmember{}c).  f[x]))
12.  c  :  bag(T)
13.  \mSigma{}(x\mmember{}firstn(||L||  -  1;L)).  f[x]  \mmember{}  R
14.  v  :  R
\mvdash{}  (v  add  \mSigma{}(x\mmember{}\{last(L)\}  +  c).  f[x])  =  ((v  add  \mSigma{}(x\mmember{}\{last(L)\}).  f[x])  add  \mSigma{}(x\mmember{}c).  f[x])


By

---

Latex:
(D  4
  THEN  DupHyp  4
  THEN  Unfold  `assoc`  -1
  THEN  (RWO  "-1<"  0  THENM  EqCD)
  THEN  Auto
  THEN  RepUR  ``bag-append  bag-summation  bag-accum``  0
  THEN  (RWO  "list\_accum\_append"  0  THENA  Auto)
  THEN  RepUR  ``single-bag``  0
  THEN  GenConclAtAddr  [2;2])

---

Home Index