---

Step * of Lemma bag-null-filter

∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[b:bag(T)].  uiff(↑bag-null([x∈b|p[x]]);∀x:T. (x ↓∈ b ⇒ (¬↑p[x])))
BY
{ ((UnivCD THENA Auto)
   THEN (BagToList (-1) THENA Auto)
   THEN ListInd (-1)
   THEN Try (Fold `empty-bag` 0)
   THEN Try (Fold `cons-bag` 0)
   THEN Reduce 0
   THEN Try (Complete ((Auto THEN BagMemberD (-1))))
   THEN AutoSplit
   THEN Auto) }

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

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

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

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (BagToList  (-1)  THENA  Auto)
  THEN  ListInd  (-1)
  THEN  Try  (Fold  `empty-bag`  0)
  THEN  Try  (Fold  `cons-bag`  0)
  THEN  Reduce  0
  THEN  Try  (Complete  ((Auto  THEN  BagMemberD  (-1))))
  THEN  AutoSplit
  THEN  Auto)

---

Home Index