---

Step * of Lemma bag-filter-empty-iff

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff(∀x:T. (x ↓∈ b ⇒ (¬↑P[x]));↑bag-null([x∈b|P[x]]))
BY
{ ((UnivCD THENA Auto)
   THEN (BagInd (-1) THENA Auto)
   THEN Folds  ``empty-bag cons-bag`` 0
   THEN Reduce 0
   THEN Try ((RWO "bag-member-empty-iff" 0 THEN Auto))
   THEN (RWO "bag-member-cons" 0 THENA Auto)
   THEN AutoSplit⋅
   THEN Try ((Auto THEN InstHyp [⌜u⌝] (-1)⋅ THEN Auto)⋅)
   THEN RWO "-1<" 0
   THEN Auto) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. ¬↑P[u]
5. v : T List
6. ∀x:T. (x ↓∈ v ⇒ (¬↑P[x]))
7. x : T
8. (x = u ∈ T) ↓∨ x ↓∈ v
9. ↑bag-null([x∈v|P[x]])
10. ∀x:T. (x ↓∈ v ⇒ (¬↑P[x]))
⊢ ¬↑P[x]

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagInd  (-1)  THENA  Auto)
  THEN  Folds    ``empty-bag  cons-bag``  0
  THEN  Reduce  0
  THEN  Try  ((RWO  "bag-member-empty-iff"  0  THEN  Auto))
  THEN  (RWO  "bag-member-cons"  0  THENA  Auto)
  THEN  AutoSplit\mcdot{}
  THEN  Try  ((Auto  THEN  InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)\mcdot{})
  THEN  RWO  "-1<"  0
  THEN  Auto)

---

Home Index