---

Step * of Lemma fan-implies-nwkl!-using-PFan

Fan ⇒ nWKL!
BY
{ (Auto THEN D 0 THEN Auto THEN InstLemma `fan-implies-PFan` [] THEN Auto) }

1
1. Fan
2. A : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(A as)
4. infinite-tree(A)
5. eff-unique(A)
6. PFan{i:l}()
⊢ ∃f:ℕ ⟶ 𝔹. is-path(A;f)

---

Latex:

---

Latex:
Fan  {}\mRightarrow{}  nWKL!


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto  THEN  InstLemma  `fan-implies-PFan`  []  THEN  Auto)

---

Home Index