---

Step * of Lemma bag-restrict-disjoint

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[b:bag(T)].  (b|x) ~ {} supposing ¬x ↓∈ b
BY
{ (Auto
   THEN BLemma `equal-empty-bag`
   THEN Auto
   THEN BagToList 4
   THEN Auto
   THEN RWO  "bag-member-list" (-1)
   THEN Auto
   THEN RepUR ``bag-restrict bag-filter empty-bag`` 0⋅) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. b : T List
5. ¬(x ∈ b)
⊢ filter(λz.(eq x z);b) = [] ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[b:bag(T)].    (b|x)  \msim{}  \{\}  supposing  \mneg{}x  \mdownarrow{}\mmember{}  b


By

---

Latex:
(Auto
  THEN  BLemma  `equal-empty-bag`
  THEN  Auto
  THEN  BagToList  4
  THEN  Auto
  THEN  RWO    "bag-member-list"  (-1)
  THEN  Auto
  THEN  RepUR  ``bag-restrict  bag-filter  empty-bag``  0\mcdot{})

---

Home Index