---

Step * 1 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. a : A
⊢ accumulate (with value s and list item x):
   f[x] + s
  over list:
    a1 @ [a]
  with starting value:
   0)
= accumulate (with value s and list item x):
   f[x] + s
  over list:
    [a / a1]
  with starting value:
   0)
∈ ℤ
BY
{ ((GenConcl ⌜0 = n ∈ ℤ⌝⋅ THENA Auto) THEN Thin (-1) THEN MoveToConcl (-1)) }

1
1. A : Type
2. f : A ⟶ ℤ
3. as : A List
4. bs : A List
5. permutation(A;as;bs)
6. a1 : A List
7. a : A
⊢ ∀n:ℤ
    (accumulate (with value s and list item x):
      f[x] + s
     over list:
       a1 @ [a]
     with starting value:
      n)
    = accumulate (with value s and list item x):
       f[x] + s
      over list:
        [a / a1]
      with starting value:
       n)
    ∈ ℤ)

---

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.  a  :  A
\mvdash{}  accumulate  (with  value  s  and  list  item  x):
      f[x]  +  s
    over  list:
        a1  @  [a]
    with  starting  value:
      0)
=  accumulate  (with  value  s  and  list  item  x):
      f[x]  +  s
    over  list:
        [a  /  a1]
    with  starting  value:
      0)


By

---

Latex:
((GenConcl  \mkleeneopen{}0  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  MoveToConcl  (-1))

---

Home Index