---

Step * 1 of Lemma bar-separation-implies-twkl!

.....assertion..... 
1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. ∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))
5. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
6. Decidable(A)
⊢ ¬tbar(T;¬(A))
BY
{ ((Assert ∀as:T List. (¬¬(A as) ⇐⇒ A as) BY
          (All (Unfold `dec-predicate`) THEN Auto THEN SupposeNot))
   THEN (D 0 THENA Auto)
   THEN (D 4 With ⌜¬(A)⌝  THENA Auto)
   THEN DVar `A'
   THEN (D -1 THENA (D 0 THEN EAuto 1))
   THEN D -1
   THEN RepeatFor 3 (ParallelOp -4)
   THEN (RepeatFor 2 (ParallelLast) ORELSE ParallelOp -4)
   THEN RepUR ``predicate-not`` 0
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  \mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size
3.  BarSep(T;T)
4.  \mforall{}A:(T  List)  {}\mrightarrow{}  \mBbbP{}.  (dbar(T;A)  {}\mRightarrow{}  (\mneg{}(down-closed(T;\mneg{}(A))  \mwedge{}  Unbounded(\mneg{}(A)))))
5.  A  :  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
6.  Decidable(A)
\mvdash{}  \mneg{}tbar(T;\mneg{}(A))


By

---

Latex:
((Assert  \mforall{}as:T  List.  (\mneg{}\mneg{}(A  as)  \mLeftarrow{}{}\mRightarrow{}  A  as)  BY
                (All  (Unfold  `dec-predicate`)  THEN  Auto  THEN  SupposeNot))
  THEN  (D  0  THENA  Auto)
  THEN  (D  4  With  \mkleeneopen{}\mneg{}(A)\mkleeneclose{}    THENA  Auto)
  THEN  DVar  `A'
  THEN  (D  -1  THENA  (D  0  THEN  EAuto  1))
  THEN  D  -1
  THEN  RepeatFor  3  (ParallelOp  -4)
  THEN  (RepeatFor  2  (ParallelLast)  ORELSE  ParallelOp  -4)
  THEN  RepUR  ``predicate-not``  0
  THEN  Auto)

---

Home Index