---

Step * 1 1 2 2 of Lemma bag-map-combine


1. A : Type
2. B : Type
3. C : Type
4. g : A ⟶ bag(B)
5. f : B ⟶ C
6. u : A
7. v : A List
8. bag-map(f;⋃x∈v.g[x]) = ⋃x∈v.bag-map(f;g[x]) ∈ bag(C)
⊢ bag-map(f;⋃x∈{u} + v.g[x]) = ⋃x∈{u} + v.bag-map(f;g[x]) ∈ bag(C)
BY
{ ((Assert v ∈ bag(A) BY
          Auto)
   THEN (RWW "bag-combine-append-left bag-map-append" 0 THENA (Auto THEN DoSubsume THEN Auto))
   THEN EqCD
   THEN Auto
   THEN Unfold `single-bag` 0
   THEN RWO "bag-combine-unit-left" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  g  :  A  {}\mrightarrow{}  bag(B)
5.  f  :  B  {}\mrightarrow{}  C
6.  u  :  A
7.  v  :  A  List
8.  bag-map(f;\mcup{}x\mmember{}v.g[x])  =  \mcup{}x\mmember{}v.bag-map(f;g[x])
\mvdash{}  bag-map(f;\mcup{}x\mmember{}\{u\}  +  v.g[x])  =  \mcup{}x\mmember{}\{u\}  +  v.bag-map(f;g[x])


By

---

Latex:
((Assert  v  \mmember{}  bag(A)  BY
                Auto)
  THEN  (RWW  "bag-combine-append-left  bag-map-append"  0  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  EqCD
  THEN  Auto
  THEN  Unfold  `single-bag`  0
  THEN  RWO  "bag-combine-unit-left"  0
  THEN  Auto)

---

Home Index