---

Step * 2 of Lemma decidable__squash_exists_fset


1. [T] : Type
2. [P] : T ⟶ ℙ
3. eq : EqDecider(T)
4. s : fset(T)
5. d : ∀x:T. Dec(P[x])
6. ∀x:T. (isl(d x) ∈ 𝔹)
7. ∀x:T. (↑isl(d x) ⇐⇒ P[x])
8. ¬¬↑fset-null({x ∈ s | isl(d x)})
⊢ ¬↓∃x:T. (x ∈ s ∧ P[x])
BY
{ ((ParallelLast THEN (D 0 THENA Auto) THEN SqExRepD)
   THEN (RWO  "assert-fset-null" (-1) THENA Auto)
   THEN (Assert x ∈ {x ∈ s | isl(d x)} BY
               (BLemma `member-fset-filter` THEN Auto))) }

1
1. T : Type
2. P : T ⟶ ℙ
3. eq : EqDecider(T)
4. s : fset(T)
5. d : ∀x:T. Dec(P[x])
6. ∀x:T. (isl(d x) ∈ 𝔹)
7. ∀x:T. (↑isl(d x) ⇐⇒ P[x])
8. x : T
9. x ∈ s
10. P[x]
11. {x ∈ s | isl(d x)} = {} ∈ fset(T)
12. x ∈ {x ∈ s | isl(d x)}
⊢ False

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  eq  :  EqDecider(T)
4.  s  :  fset(T)
5.  d  :  \mforall{}x:T.  Dec(P[x])
6.  \mforall{}x:T.  (isl(d  x)  \mmember{}  \mBbbB{})
7.  \mforall{}x:T.  (\muparrow{}isl(d  x)  \mLeftarrow{}{}\mRightarrow{}  P[x])
8.  \mneg{}\mneg{}\muparrow{}fset-null(\{x  \mmember{}  s  |  isl(d  x)\})
\mvdash{}  \mneg{}\mdownarrow{}\mexists{}x:T.  (x  \mmember{}  s  \mwedge{}  P[x])


By

---

Latex:
((ParallelLast  THEN  (D  0  THENA  Auto)  THEN  SqExRepD)
  THEN  (RWO    "assert-fset-null"  (-1)  THENA  Auto)
  THEN  (Assert  x  \mmember{}  \{x  \mmember{}  s  |  isl(d  x)\}  BY
                          (BLemma  `member-fset-filter`  THEN  Auto)))

---

Home Index