---

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

.....debug..... 
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)
8. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ ...EqCDAux1... bag-accum(b,x.{f[x]} + b;{};bag-accum(b,x.if P[x] then {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 ;{};v + {u}))
∈ bag(B)
BY
{ (RemoveLabel THEN Using [`T',⌜{x:A| ↑P[x]} ⌝] MemCD⋅ THEN Auto) }

1
.....subterm..... T:t
3:n
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)
8. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ bag-accum(b,x.if P[x] then {x} + b else b fi ;{};{u} + v)
= bag-accum(b,x.if P[x] then {x} + b else b fi ;{};v + {u})
∈ bag({x:A| ↑P[x]} )

---

Latex:

---

Latex:
.....debug..... 
1.  A  :  Type
2.  B  :  Type
3.  P  :  A  {}\mrightarrow{}  \mBbbB{}
4.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  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))
8.  (\{u\}  +  v)  =  (v  +  \{u\})
\mvdash{}  ...EqCDAux1...  bag-accum(b,x.\{f[x]\}  +  b;\{\};bag-accum(b,x.if  P[x]  then  \{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  ;\{\};v  +  \{u\}))


By

---

Latex:
(RemoveLabel  THEN  Using  [`T',\mkleeneopen{}\{x:A|  \muparrow{}P[x]\}  \mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto)

---

Home Index