---

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

nWKL! ⇐⇒ WKL!(𝔹)
BY
{ (RepUR ``nwkl! twkl! eff-unique`` 0
   THEN Folds ``dec-predicate eff-unique-path`` 0
   THEN Auto
   THEN InstHyp [⌜A⌝] 1⋅
   THEN Auto
   THEN Try (((D (-1) THEN With ⌜f⌝ (D 0)⋅) THEN Auto))) }

1
.....antecedent..... 
1. ∀A:(𝔹 List) ⟶ ℙ. (Decidable(A) ⇒ infinite-tree(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:ℕ ⟶ 𝔹. is-path(A;f)))
2. A : {A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
3. Decidable(A)
4. eff-unique-path(𝔹;A)
⊢ infinite-tree(A)

2
.....wf..... 
1. ∀A:{A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
     (Decidable(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:{ℕ ⟶ 𝔹| is-path(A;f)}))
2. A : (𝔹 List) ⟶ ℙ
3. Decidable(A)
4. infinite-tree(A)
5. eff-unique-path(𝔹;A)
⊢ A ∈ {A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 

3
1. ∀A:{A:(𝔹 List) ⟶ ℙ| down-closed(𝔹;A) ∧ Unbounded(A)} 
     (Decidable(A) ⇒ eff-unique-path(𝔹;A) ⇒ (∃f:{ℕ ⟶ 𝔹| is-path(A;f)}))
2. A : (𝔹 List) ⟶ ℙ
3. Decidable(A)
4. infinite-tree(A)
5. eff-unique-path(𝔹;A)
6. f : ℕ ⟶ 𝔹
7. [%9] : is-path(A;f)
⊢ is-path(A;f)

---

Latex:

---

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


By

---

Latex:
(RepUR  ``nwkl!  twkl!  eff-unique``  0
  THEN  Folds  ``dec-predicate  eff-unique-path``  0
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}A\mkleeneclose{}]  1\mcdot{}
  THEN  Auto
  THEN  Try  (((D  (-1)  THEN  With  \mkleeneopen{}f\mkleeneclose{}  (D  0)\mcdot{})  THEN  Auto)))

---

Home Index