---

Step * of Lemma bag-filter_wf

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  ([x∈bs|p[x]] ∈ bag({x:T| ↑p[x]} ))
BY
{ (Auto
   THEN BagD (-1)
   THEN Auto
   THEN Unfold `bag-filter` 0
   THEN EqTypeCD
   THEN Try (((Subst ⌜{x:T| ↑p[x]}  ~ {x:T| ↑λx.p[x][x]} ⌝ 0⋅ THENA (RepUR ``so_apply`` 0 THEN Auto))
              THEN BLemma `filter_type`
              THEN Auto))) }

1
.....wf..... 
1. T : Type
2. p : T ⟶ 𝔹
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
⊢ {x:T| ↑p[x]}  List ∈ Type

2
.....wf..... 
1. T : Type
2. p : T ⟶ 𝔹
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
⊢ λas,bs. permutation({x:T| ↑p[x]} ;as;bs) ∈ ({x:T| ↑p[x]}  List) ⟶ ({x:T| ↑p[x]}  List) ⟶ ℙ

3
.....aux..... 
1. T : Type
2. p : T ⟶ 𝔹
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
⊢ EquivRel({x:T| ↑p[x]}  List;x,y.permutation({x:T| ↑p[x]} ;x;y))

4
.....antecedent..... 
1. T : Type
2. p : T ⟶ 𝔹
3. as : T List
4. bs : T List
5. permutation(T;as;bs)
⊢ permutation({x:T| ↑p[x]} ;filter(λx.p[x];as);filter(λx.p[x];bs))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    ([x\mmember{}bs|p[x]]  \mmember{}  bag(\{x:T|  \muparrow{}p[x]\}  ))


By

---

Latex:
(Auto
  THEN  BagD  (-1)
  THEN  Auto
  THEN  Unfold  `bag-filter`  0
  THEN  EqTypeCD
  THEN  Try  (((Subst  \mkleeneopen{}\{x:T|  \muparrow{}p[x]\}    \msim{}  \{x:T|  \muparrow{}\mlambda{}x.p[x][x]\}  \mkleeneclose{}  0\mcdot{}  THENA  (RepUR  ``so\_apply``  0  THEN  Auto))
                        THEN  BLemma  `filter\_type`
                        THEN  Auto)))

---

Home Index