---

Step * 1 1 of Lemma bag-filter-union

.....equality..... 
1. T : Type
2. p : T ⟶ 𝔹
3. as : bag(T) List
4. bs : bag(T) List
5. permutation(bag(T);as;bs)
⊢ bag-union(bag-map(λb.[x∈b|p[x]];bs)) ~ [x∈bag-union(bs)|p[x]]
BY
{ (GenConcl ⌜bs = L ∈ (Top List List)⌝⋅ THEN Auto)⋅ }

1
1. T : Type
2. p : T ⟶ 𝔹
3. as : bag(T) List
4. bs : bag(T) List
5. permutation(bag(T);as;bs)
6. L : Top List List
7. bs = L ∈ (Top List List)
⊢ bag-union(bag-map(λb.[x∈b|p[x]];L)) ~ [x∈bag-union(L)|p[x]]

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  as  :  bag(T)  List
4.  bs  :  bag(T)  List
5.  permutation(bag(T);as;bs)
\mvdash{}  bag-union(bag-map(\mlambda{}b.[x\mmember{}b|p[x]];bs))  \msim{}  [x\mmember{}bag-union(bs)|p[x]]


By

---

Latex:
(GenConcl  \mkleeneopen{}bs  =  L\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index