---

Step * 1 1 1 of Lemma bag-filter-union


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]]
BY
{ (RepUR ``bag-filter bag-union bag-map concat`` 0 THEN All Thin)⋅ }

1
1. T : Type
2. p : T ⟶ 𝔹
3. L : Top List List
⊢ reduce(λl,l'. (l @ l');[];map(λb.filter(λx.p[x];b);L)) ~ filter(λx.p[x];reduce(λl,l'. (l @ l');[];L))

---

Latex:

---

Latex:

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


By

---

Latex:
(RepUR  ``bag-filter  bag-union  bag-map  concat``  0  THEN  All  Thin)\mcdot{}

---

Home Index