---

Step * of Lemma bag-combine-as-accum

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[bs:bag(A)].  (⋃b∈bs.f[b] = bag-accum(c,b.f[b] + c;{};bs) ∈ bag(B))
BY
{ (Auto THEN BagInd (-1) THEN Auto) }

1
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
⊢ ⋃b∈[].f[b] = bag-accum(c,b.f[b] + c;{};[]) ∈ bag(B)

2
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. u : A
5. v : A List
6. ⋃b∈v.f[b] = bag-accum(c,b.f[b] + c;{};v) ∈ bag(B)
⊢ ⋃b∈[u / v].f[b] = bag-accum(c,b.f[b] + c;{};[u / v]) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[bs:bag(A)].    (\mcup{}b\mmember{}bs.f[b]  =  bag-accum(c,b.f[b]  +  c;\{\};bs))


By

---

Latex:
(Auto  THEN  BagInd  (-1)  THEN  Auto)

---

Home Index