---

Step * 1 of Lemma assert-fset-contains-none-of


1. T : Type
2. eq : EqDecider(T)
3. s : fset(T)
4. cs : fset(fset(T))
5. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff({x ∈ s | P[x]} = {} ∈ fset(fset(T));¬(∃x:fset(T). (x ∈ s ∧ (↑P[x]))))
6. ∀c:fset(T). (c ∈ cs ⇒ (¬c ⊆ s))
⊢ ¬(∃c:fset(T). (c ∈ cs ∧ (↑(deq-f-subset(eq) c s))))
BY
{ ((D 0 THENA Auto) THEN ExRepD THEN RW assert_pushdownC (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  s  :  fset(T)
4.  cs  :  fset(fset(T))
5.  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(fset(T))].
          uiff(\{x  \mmember{}  s  |  P[x]\}  =  \{\};\mneg{}(\mexists{}x:fset(T).  (x  \mmember{}  s  \mwedge{}  (\muparrow{}P[x]))))
6.  \mforall{}c:fset(T).  (c  \mmember{}  cs  {}\mRightarrow{}  (\mneg{}c  \msubseteq{}  s))
\mvdash{}  \mneg{}(\mexists{}c:fset(T).  (c  \mmember{}  cs  \mwedge{}  (\muparrow{}(deq-f-subset(eq)  c  s))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  ExRepD  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index