---

Step * of Lemma bag-sum-count

∀[A,B:Type]. ∀[f:B ⟶ bag(A)]. ∀[eq:EqDecider(A)]. ∀[bb:bag(B)]. ∀[z:A].
  (bag-sum(bb;b.(#z in f[b])) ~ bag-sum([b∈bb|1 ≤z (#z in f[b])];b.(#z in f[b])))
BY
{ ((Auto THEN BagD (-2)) THEN Auto THEN Subst ⌜as = bs ∈ bag(B)⌝ 0⋅ THEN Auto) }

1
1. A : Type
2. B : Type
3. f : B ⟶ bag(A)
4. eq : EqDecider(A)
5. z : A
6. as : B List
7. bs : B List
8. permutation(B;as;bs)
⊢ bag-sum(bs;b.(#z in f[b])) = bag-sum([b∈bs|1 ≤z (#z in f[b])];b.(#z in f[b])) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:B  {}\mrightarrow{}  bag(A)].  \mforall{}[eq:EqDecider(A)].  \mforall{}[bb:bag(B)].  \mforall{}[z:A].
    (bag-sum(bb;b.(\#z  in  f[b]))  \msim{}  bag-sum([b\mmember{}bb|1  \mleq{}z  (\#z  in  f[b])];b.(\#z  in  f[b])))


By

---

Latex:
((Auto  THEN  BagD  (-2))  THEN  Auto  THEN  Subst  \mkleeneopen{}as  =  bs\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index