---

Step * of Lemma bag-filter-empty

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  ∀x:T. (x ↓∈ b ⇒ (¬↑P[x])) supposing ↑bag-null([x∈b|P[x]])
BY
{ ((UnivCD THENA Auto)
   THEN (D 0 THENA Auto)
   THEN Unfold `bag-member` (-2)
   THEN SquashExRepD
   THEN (RevHypSubst' (-3) (-6) THENA (Auto THEN RepUR ``bag-null bag-filter`` 0 THEN Auto))
   THEN ThinVar `b'
   THEN RepUR ``bag-null bag-filter`` (-1)
   THEN (RWO "assert_of_null" (-1) THENA Auto)
   THEN (InstLemma `member-filter` [⌜T⌝;⌜P⌝;⌜L⌝;⌜x⌝]⋅ THENA Auto)
   THEN (RepeatFor 2 (D (-1)) THENA Auto)
   THEN (FLemma `sqequal-nil` [-3]⋅ THENA Auto)
   THEN HypSubst (-1) (-2)
   THEN GenListD (-2)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[b:bag(T)].    \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\mneg{}\muparrow{}P[x]))  supposing  \muparrow{}bag-null([x\mmember{}b|P[x]])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `bag-member`  (-2)
  THEN  SquashExRepD
  THEN  (RevHypSubst'  (-3)  (-6)  THENA  (Auto  THEN  RepUR  ``bag-null  bag-filter``  0  THEN  Auto))
  THEN  ThinVar  `b'
  THEN  RepUR  ``bag-null  bag-filter``  (-1)
  THEN  (RWO  "assert\_of\_null"  (-1)  THENA  Auto)
  THEN  (InstLemma  `member-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RepeatFor  2  (D  (-1))  THENA  Auto)
  THEN  (FLemma  `sqequal-nil`  [-3]\mcdot{}  THENA  Auto)
  THEN  HypSubst  (-1)  (-2)
  THEN  GenListD  (-2))

---

Home Index