---

Step * of Lemma bag-combine-eq-right

∀[A,B:Type]. ∀[b:bag(A)]. ∀[f1,f2:A ⟶ bag(B)].
  ⋃x∈b.f1[x] = ⋃x∈b.f2[x] ∈ bag(B) supposing ∀x:{x:A| x ↓∈ b} . (f1[x] = f2[x] ∈ bag(B))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``bag-combine`` 0
   THEN (Assert ⌜bag-map(λx.f1[x];b) = bag-map(λx.f2[x];b) ∈ bag(bag(B))⌝⋅ THENM (RWO "-1" 0 THEN Auto))
   THEN (BagToList (-4) THENA Auto)
   THEN RepUR ``bag-map`` 0) }

1
1. A : Type
2. B : Type
3. b : A List
4. f1 : A ⟶ bag(B)
5. f2 : A ⟶ bag(B)
6. ∀x:{x:A| x ↓∈ b} . (f1[x] = f2[x] ∈ bag(B))
⊢ map(λx.f1[x];b) = map(λx.f2[x];b) ∈ bag(bag(B))

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[b:bag(A)].  \mforall{}[f1,f2:A  {}\mrightarrow{}  bag(B)].
    \mcup{}x\mmember{}b.f1[x]  =  \mcup{}x\mmember{}b.f2[x]  supposing  \mforall{}x:\{x:A|  x  \mdownarrow{}\mmember{}  b\}  .  (f1[x]  =  f2[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``bag-combine``  0
  THEN  (Assert  \mkleeneopen{}bag-map(\mlambda{}x.f1[x];b)  =  bag-map(\mlambda{}x.f2[x];b)\mkleeneclose{}\mcdot{}  THENM  (RWO  "-1"  0  THEN  Auto))
  THEN  (BagToList  (-4)  THENA  Auto)
  THEN  RepUR  ``bag-map``  0)

---

Home Index