---

Step * 1 of Lemma bag-filter-is-empty


1. T : Type
2. P : T ⟶ 𝔹
3. b : bag(T)
4. ∀x:T. (x ↓∈ b ⇒ (¬↑P[x]))
5. ↑bag-null([x∈b|P[x]])
⊢ [x∈b|P[x]] = {} ∈ bag(T)
BY
{ (RW assert_pushdownC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  b  :  bag(T)
4.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\mneg{}\muparrow{}P[x]))
5.  \muparrow{}bag-null([x\mmember{}b|P[x]])
\mvdash{}  [x\mmember{}b|P[x]]  =  \{\}


By

---

Latex:
(RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index