---

Step * 2 1 of Lemma bag-combine-as-accum


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)
⊢ (f[u] + bag-accum(c,b.f[b] + c;{};v)) = bag-accum(c,b.f[b] + c;{};u.v) ∈ bag(B)
BY
{ ((RWO "cons-bag-as-append" 0 THENA Auto)
   THEN (InstLemma `bag-append-comm` [⌜A⌝;⌜{u}⌝;⌜v⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)) }

1
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)
7. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ (f[u] + bag-accum(c,b.f[b] + c;{};v)) = bag-accum(c,b.f[b] + c;{};v + {u}) ∈ bag(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  u  :  A
5.  v  :  A  List
6.  \mcup{}b\mmember{}v.f[b]  =  bag-accum(c,b.f[b]  +  c;\{\};v)
\mvdash{}  (f[u]  +  bag-accum(c,b.f[b]  +  c;\{\};v))  =  bag-accum(c,b.f[b]  +  c;\{\};u.v)


By

---

Latex:
((RWO  "cons-bag-as-append"  0  THENA  Auto)
  THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\{u\}\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index