---

Step * of Lemma bag-count-combine

∀[T1,T2:Type]. ∀[f:T1 ⟶ bag(T2)]. ∀[eq:EqDecider(T2)]. ∀[z:T2]. ∀[bs:bag(T1)].
  ((#z in ⋃x∈bs.f[x]) ~ bag-sum(bs;x.(#z in f[x])))
BY
{ (Auto
   THEN BagD (-1)
   THEN Auto
   THEN (Subst ⌜as = bs ∈ bag(T1)⌝ 0⋅ THENA Auto)
   THEN ThinVar `as'
   THEN RenameVar `L' (-1)) }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq : EqDecider(T2)
5. z : T2
6. L : T1 List
⊢ (#z in ⋃x∈L.f[x]) = bag-sum(L;x.(#z in f[x])) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[f:T1  {}\mrightarrow{}  bag(T2)].  \mforall{}[eq:EqDecider(T2)].  \mforall{}[z:T2].  \mforall{}[bs:bag(T1)].
    ((\#z  in  \mcup{}x\mmember{}bs.f[x])  \msim{}  bag-sum(bs;x.(\#z  in  f[x])))


By

---

Latex:
(Auto
  THEN  BagD  (-1)
  THEN  Auto
  THEN  (Subst  \mkleeneopen{}as  =  bs\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  ThinVar  `as'
  THEN  RenameVar  `L'  (-1))

---

Home Index