---

Step * 2 1 1 of Lemma Accum-loc-class-as-loop-class2


1. B : Type
2. A : Type
3. v1 : bag(B)@i
4. v2 : bag(A)@i
5. z : A ─→ B ─→ B@i
⊢ ∪f@0∈bag-map(z;v2).bag-map(f@0;v1) = ∪x∈v2.∪x@0∈v1.{z x x@0} ∈ bag(B)
BY
{ ((RWO "bag-combine-map" 0 THENA Auto) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  Type
2.  A  :  Type
3.  v1  :  bag(B)@i
4.  v2  :  bag(A)@i
5.  z  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  B@i
\mvdash{}  \mcup{}f@0\mmember{}bag-map(z;v2).bag-map(f@0;v1)  =  \mcup{}x\mmember{}v2.\mcup{}x@0\mmember{}v1.\{z  x  x@0\}


By

---

Latex:
((RWO  "bag-combine-map"  0  THENA  Auto)  THEN  EqCD  THEN  Auto)

---

Home Index