---

Step * of Lemma alt-bar-sep-wkl!

∀[T:Type]
  ((∃size:ℕ. T ~ ℕsize)
  ⇒ BarSep(T;T)
  ⇒ (∀A:{A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} . (¬bar(¬(A))))
  ⇒ WKL!(T))
BY
{ ((Auto THEN RepeatFor 2 ((D 0 THENA Auto)))
   THEN (D -3 With ⌜A⌝  THENA Auto)
   THEN PromoteHyp (-1) 5
   THEN (Assert Tree(A) BY
               (DVar `A' THEN Unhide THEN Auto THEN Unfold `alttree` 0 THEN Auto))
   THEN D 2
   THEN (Assert 0 < size BY
               ((CaseNat 0 `size' THEN Auto)
                THEN (Assert ⌜False⌝⋅ THEN Auto)
                THEN DVar `A'
                THEN Auto
                THEN D 3
                THEN (D -5 With ⌜1⌝  THENA Auto)
                THEN ExRepD
                THEN (Assert f (s 0) ∈ ℕsize BY
                            Auto)
                THEN MemTypeHD (-1)
                THEN Auto))
   THEN (Assert T BY
               (D 3 THEN D 4 THEN With ⌜0⌝ (D 5)⋅ THEN ExRepD THEN Auto))
   THEN (Assert ∀a,b:T.  Dec(a = b ∈ T) BY
               (Auto
                THEN D 3
                THEN (Decide ⌜(f a) = (f b) ∈ ℕsize⌝⋅ THENA Auto)
                THEN Try ((OrLeft THEN Complete (Auto)))
                THEN (OrRight THEN Auto)⋅
                THEN ParallelLast
                THEN Auto))
   THEN (Assert ∃L:T List. ∀x:T. (x ∈ L) BY
               ((BLemma `finite-type-iff-list` THENM D 0 With ⌜size⌝ )
                THEN Auto
                THEN (FLemma `equipollent_inversion` [3] THENM (RepeatFor 2 (D (-1)) THEN With ⌜f⌝ (D 0)⋅ THEN Auto))
                THEN Auto))
   THEN ThinVar `size'
   THEN RenameVar `t0' (-3)
   THEN ExRepD
   THEN (Assert ¬↑null(L) BY
               (DVar `L'
                THEN Reduce 0
                THEN Auto
                THEN With ⌜t0⌝ (D (-1))⋅
                THEN Auto
                THEN RWO "nil_member" (-1)
                THEN Auto))) }

1
1. [T] : Type
2. BarSep(T;T)
3. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. L : T List
10. ∀x:T. (x ∈ L)
11. ¬↑null(L)
⊢ ∃f:ℕ ⟶ T [IsPath(A;f)]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size)
    {}\mRightarrow{}  BarSep(T;T)
    {}\mRightarrow{}  (\mforall{}A:\{A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}|  Tree(A)  \mwedge{}  Unbounded(A)\}  .  (\mneg{}bar(\mneg{}(A))))
    {}\mRightarrow{}  WKL!(T))


By

---

Latex:
((Auto  THEN  RepeatFor  2  ((D  0  THENA  Auto)))
  THEN  (D  -3  With  \mkleeneopen{}A\mkleeneclose{}    THENA  Auto)
  THEN  PromoteHyp  (-1)  5
  THEN  (Assert  Tree(A)  BY
                          (DVar  `A'  THEN  Unhide  THEN  Auto  THEN  Unfold  `alttree`  0  THEN  Auto))
  THEN  D  2
  THEN  (Assert  0  <  size  BY
                          ((CaseNat  0  `size'  THEN  Auto)
                            THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
                            THEN  DVar  `A'
                            THEN  Auto
                            THEN  D  3
                            THEN  (D  -5  With  \mkleeneopen{}1\mkleeneclose{}    THENA  Auto)
                            THEN  ExRepD
                            THEN  (Assert  f  (s  0)  \mmember{}  \mBbbN{}size  BY
                                                    Auto)
                            THEN  MemTypeHD  (-1)
                            THEN  Auto))
  THEN  (Assert  T  BY
                          (D  3  THEN  D  4  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  5)\mcdot{}  THEN  ExRepD  THEN  Auto))
  THEN  (Assert  \mforall{}a,b:T.    Dec(a  =  b)  BY
                          (Auto
                            THEN  D  3
                            THEN  (Decide  \mkleeneopen{}(f  a)  =  (f  b)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  Try  ((OrLeft  THEN  Complete  (Auto)))
                            THEN  (OrRight  THEN  Auto)\mcdot{}
                            THEN  ParallelLast
                            THEN  Auto))
  THEN  (Assert  \mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L)  BY
                          ((BLemma  `finite-type-iff-list`  THENM  D  0  With  \mkleeneopen{}size\mkleeneclose{}  )
                            THEN  Auto
                            THEN  (FLemma  `equipollent\_inversion`  [3]
                            THENM  (RepeatFor  2  (D  (-1))  THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
                            )
                            THEN  Auto))
  THEN  ThinVar  `size'
  THEN  RenameVar  `t0'  (-3)
  THEN  ExRepD
  THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                          (DVar  `L'
                            THEN  Reduce  0
                            THEN  Auto
                            THEN  With  \mkleeneopen{}t0\mkleeneclose{}  (D  (-1))\mcdot{}
                            THEN  Auto
                            THEN  RWO  "nil\_member"  (-1)
                            THEN  Auto)))

---

Home Index