---

Step * of Lemma decidable__squash_exists_fset

∀[T:Type]. ∀[P:T ⟶ ℙ].  ∀eq:EqDecider(T). ∀s:fset(T).  ((∀x:T. Dec(P[x])) ⇒ Dec(↓∃x:T. (x ∈ s ∧ P[x])))
BY
{ (Auto
   THEN RenameVar `d' (-1)
   THEN (Assert ∀x:T. (isl(d x) ∈ 𝔹) BY
               ((D 0 THENA Auto) THEN Try ((GenConclTerm ⌜d x⌝⋅ THEN Auto)) THEN Auto))
   THEN (Assert ∀x:T. (↑isl(d x) ⇐⇒ P[x]) BY
               ((D 0 THENA Auto) THEN GenConclTerm ⌜d x⌝⋅ THEN Auto THEN D -3 THEN Reduce 0 THEN Auto))
   THEN (Assert ⌜Dec(¬↑fset-null({x ∈ s | isl(d x)}))⌝⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)) }

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. ¬↑fset-null({x ∈ s | isl(d x)})
⊢ ↓∃x:T. (x ∈ s ∧ P[x])

2
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])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}eq:EqDecider(T).  \mforall{}s:fset(T).    ((\mforall{}x:T.  Dec(P[x]))  {}\mRightarrow{}  Dec(\mdownarrow{}\mexists{}x:T.  (x  \mmember{}  s  \mwedge{}  P[x])))


By

---

Latex:
(Auto
  THEN  RenameVar  `d'  (-1)
  THEN  (Assert  \mforall{}x:T.  (isl(d  x)  \mmember{}  \mBbbB{})  BY
                          ((D  0  THENA  Auto)  THEN  Try  ((GenConclTerm  \mkleeneopen{}d  x\mkleeneclose{}\mcdot{}  THEN  Auto))  THEN  Auto))
  THEN  (Assert  \mforall{}x:T.  (\muparrow{}isl(d  x)  \mLeftarrow{}{}\mRightarrow{}  P[x])  BY
                          ((D  0  THENA  Auto)
                            THEN  GenConclTerm  \mkleeneopen{}d  x\mkleeneclose{}\mcdot{}
                            THEN  Auto
                            THEN  D  -3
                            THEN  Reduce  0
                            THEN  Auto))
  THEN  (Assert  \mkleeneopen{}Dec(\mneg{}\muparrow{}fset-null(\{x  \mmember{}  s  |  isl(d  x)\}))\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast))

---

Home Index