---

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

∀[T:Type]
  ((∃size:ℕ. T ~ ℕsize)
  ⇒ BarSep(T;T)
  ⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A))))))
  ⇒ WKL!(T))
BY
{ (Auto THEN RepeatFor 2 ((D 0 THENA Auto)) THEN Assert ¬tbar(T;¬(A))⋅) }

1
.....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))

2
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)
7. ¬tbar(T;¬(A))
⊢ eff-unique-path(T;A) ⇒ (∃f:ℕ ⟶ T [is-path(A;f)])

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size)
    {}\mRightarrow{}  BarSep(T;T)
    {}\mRightarrow{}  (\mforall{}A:(T  List)  {}\mrightarrow{}  \mBbbP{}.  (dbar(T;A)  {}\mRightarrow{}  (\mneg{}(down-closed(T;\mneg{}(A))  \mwedge{}  Unbounded(\mneg{}(A))))))
    {}\mRightarrow{}  WKL!(T))


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((D  0  THENA  Auto))  THEN  Assert  \mneg{}tbar(T;\mneg{}(A))\mcdot{})

---

Home Index