---

Step * 1 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
⊢ ∀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)
    ∈ ℤ)
BY
{ (All Thin THEN ListInd (-2) THEN Reduce 0 THEN Auto THEN RWO "-2" 0 THEN Auto)⋅ }

1
1. A : Type
2. f : A ⟶ ℤ
3. a : A
4. u : A
5. v : A List
6. ∀n:ℤ
     (accumulate (with value s and list item x):
       f[x] + s
      over list:
        v @ [a]
      with starting value:
       n)
     = accumulate (with value s and list item x):
        f[x] + s
       over list:
         [a / v]
       with starting value:
        n)
     ∈ ℤ)
7. n : ℤ
⊢ accumulate (with value s and list item x):
   f[x] + s
  over list:
    [a / v]
  with starting value:
   f[u] + n)
= accumulate (with value s and list item x):
   f[x] + s
  over list:
    v
  with starting value:
   f[u] + f[a] + 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{}  \mforall{}n:\mBbbZ{}
        (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))


By

---

Latex:
(All  Thin  THEN  ListInd  (-2)  THEN  Reduce  0  THEN  Auto  THEN  RWO  "-2"  0  THEN  Auto)\mcdot{}

---

Home Index