---

Step * 1 of Lemma bag-filter-filter2


1. T : Type
2. p : T ⟶ 𝔹
3. q : {x:T| ↑p[x]}  ⟶ 𝔹
4. bs : T List
⊢ [x∈[x∈bs|p[x]]|q[x]] = [x∈bs|p[x] ∧b q[x]] ∈ bag({x:T| ↑(p[x] ∧b q[x])} )
BY
{ (RepUR ``bag-filter`` 0
   THEN RWO "filter-filter" 0
   THEN RepUR ``so_apply`` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Fold `bag-filter` 0) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  q  :  \{x:T|  \muparrow{}p[x]\}    {}\mrightarrow{}  \mBbbB{}
4.  bs  :  T  List
\mvdash{}  [x\mmember{}[x\mmember{}bs|p[x]]|q[x]]  =  [x\mmember{}bs|p[x]  \mwedge{}\msubb{}  q[x]]


By

---

Latex:
(RepUR  ``bag-filter``  0
  THEN  RWO  "filter-filter"  0
  THEN  RepUR  ``so\_apply``  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Fold  `bag-filter`  0)

---

Home Index