---

Step * 2 of Lemma bag-sum_wf


1. A : Type
2. f : A ⟶ ℤ
3. as : A List
4. bs : A List
5. permutation(A;as;bs)
6. a1 : A List
7. a1@0 : A
8. a2 : A
⊢ accumulate (with value s and list item x):
   f[x] + s
  over list:
    [a2; [a1@0 / a1]]
  with starting value:
   0)
= accumulate (with value s and list item x):
   f[x] + s
  over list:
    [a1@0; [a2 / a1]]
  with starting value:
   0)
∈ ℤ
BY
{ (Reduce 0 THEN EqCD THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbZ{}
3.  as  :  A  List
4.  bs  :  A  List
5.  permutation(A;as;bs)
6.  a1  :  A  List
7.  a1@0  :  A
8.  a2  :  A
\mvdash{}  accumulate  (with  value  s  and  list  item  x):
      f[x]  +  s
    over  list:
        [a2;  [a1@0  /  a1]]
    with  starting  value:
      0)
=  accumulate  (with  value  s  and  list  item  x):
      f[x]  +  s
    over  list:
        [a1@0;  [a2  /  a1]]
    with  starting  value:
      0)


By

---

Latex:
(Reduce  0  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index