---

Step * 1 of Lemma bag-mapfilter-fast-eq


1. A : Type
2. B : Type
3. bs : bag(A)
4. P : A ⟶ 𝔹
5. f : {x:A| ↑P[x]}  ⟶ B
⊢ bag-mapfilter-fast(f;P;bs) = bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};bs)) ∈ bag(B)
BY
{ (RepUR ``bag-mapfilter-fast`` 0 THEN (BagInd (-3) THENA Auto)) }

1
1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑P[x]}  ⟶ B
⊢ bag-accum(b,x.if P[x] then f[x].b else b fi ;{};[])
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};[]))
∈ bag(B)

2
1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑P[x]}  ⟶ B
5. u : A
6. v : A List
7. bag-accum(b,x.if P[x] then f[x].b else b fi ;{};v)
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};v))
∈ bag(B)
⊢ bag-accum(b,x.if P[x] then f[x].b else b fi ;{};[u / v])
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};[u / v]))
∈ bag(B)

3
1. A : Type
2. B : Type
3. L : A List
4. bs : bag(A)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑P[x]}  ⟶ B
7. bs = L ∈ bag(A)
8. z : bag(A)
9. b : bag(B)
10. x : A
11. y : A
⊢ if P[x] then f[x].if P[y] then f[y].b else b fi 
if P[y] then f[y].b
else b
fi 
= if P[y] then f[y].if P[x] then f[x].b else b fi 
  if P[x] then f[x].b
  else b
  fi 
∈ bag(B)

4
1. A : Type
2. B : Type
3. L : A List
4. bs : bag(A)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑P[x]}  ⟶ B
7. bs = L ∈ bag(A)
8. z : bag(A)
⊢ bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};z)) ∈ bag(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  bs  :  bag(A)
4.  P  :  A  {}\mrightarrow{}  \mBbbB{}
5.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B
\mvdash{}  bag-mapfilter-fast(f;P;bs)
=  bag-accum(b,x.f[x].b;\{\};bag-accum(b,x.if  P[x]  then  x.b  else  b  fi  ;\{\};bs))


By

---

Latex:
(RepUR  ``bag-mapfilter-fast``  0  THEN  (BagInd  (-3)  THENA  Auto))

---

Home Index