---

Step * of Lemma bag-sum_wf

∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)].  (bag-sum(ba;x.f[x]) ∈ ℤ)
BY
{ (Auto
   THEN BagD (-1)
   THEN Auto
   THEN Unfold `bag-sum` 0
   THEN (InstLemma `permutation-invariant` [⌜A⌝;⌜λ2as.accumulate (with value s and list item x):
                                                       f[x] + s
                                                      over list:
                                                        as
                                                      with starting value:
                                                       0)
                                                 = accumulate (with value s and list item x):
                                                    f[x] + s
                                                   over list:
                                                     bs
                                                   with starting value:
                                                    0)
                                                 ∈ ℤ⌝]⋅
         THENA Auto
         )
   THEN Try (((InstHyp [⌜as⌝;⌜bs⌝] (-1)⋅ THENA Auto) THEN BHyp -1  THEN Auto))
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN Thin (-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
⊢ 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)
∈ ℤ

2
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)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[ba:bag(A)].    (bag-sum(ba;x.f[x])  \mmember{}  \mBbbZ{})


By

---

Latex:
(Auto
  THEN  BagD  (-1)
  THEN  Auto
  THEN  Unfold  `bag-sum`  0
  THEN  (InstLemma  `permutation-invariant`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}as.accumulate  (with  value  s  and  list  item  x):
                                                                                                          f[x]  +  s
                                                                                                        over  list:
                                                                                                            as
                                                                                                        with  starting  value:
                                                                                                          0)
                                                                                              =  accumulate  (with  value  s  and  list  item  x):
                                                                                                    f[x]  +  s
                                                                                                  over  list:
                                                                                                      bs
                                                                                                  with  starting  value:
                                                                                                    0)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Try  (((InstHyp  [\mkleeneopen{}as\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  BHyp  -1    THEN  Auto))
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  Thin  (-1))

---

Home Index