---

Step * of Lemma wkl!-iff-twkl!-bool

WKL! ⇐⇒ WKL!(𝔹)
BY
{ (RepUR ``wkl! twkl! eff-unique infinite-tree down-closed R-closed`` 0
   THEN Folds ``dec-predicate eff-unique-path`` 0
   THEN Folds ``unbounded-list-predicate`` 0
   THEN Auto
   THEN BackThruSomeHyp
   THEN Auto) }

---

Latex:

---

Latex:
WKL!  \mLeftarrow{}{}\mRightarrow{}  WKL!(\mBbbB{})


By

---

Latex:
(RepUR  ``wkl!  twkl!  eff-unique  infinite-tree  down-closed  R-closed``  0
  THEN  Folds  ``dec-predicate  eff-unique-path``  0
  THEN  Folds  ``unbounded-list-predicate``  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index