---

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


1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. ∀as,bs:𝔹 List.  (as ≤ bs ⇒ (t bs) ⇒ (t as))
5. eff-unique(t)
6. ∀n:ℕ
     ∃k:ℕ
      ((n ≤ k)
      ∧ (∀b,c:𝔹 List.
           ((||b|| = k ∈ ℤ) ⇒ (||c|| = k ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
7. a : n:ℕ ⟶ (𝔹 List)
8. ∀n:ℕ. ((||a n|| = n ∈ ℤ) ∧ (t (a n)))
9. k0 : n:ℕ ⟶ ℕ
10. ∀n:ℕ
      ((n ≤ (k0 n))
      ∧ (∀b,c:𝔹 List.
           ((||b|| = (k0 n) ∈ ℤ) ⇒ (||c|| = (k0 n) ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
11. k : ℕ ⟶ ℤ
12. ∀i,j:ℕ.  ((i ≤ j) ⇒ ((k i) ≤ (k j)))
13. ∀n:ℕ. ((k0 n) ≤ (k n))
14. ∀n:ℕ. (n ≤ (k n))
15. ∀n:ℕ. (0 ≤ (k n))
⊢ ∃f:ℕ ⟶ 𝔹. is-path(t;f)
BY
{ ((Assert ⌜∃b:ℕ ⟶ (𝔹 List). ∀n:ℕ. ((b n) = firstn(n;a (k n)) ∈ (𝔹 List))⌝ BY
          (With ⌜λn.firstn(n;a (k n))⌝ (D 0)⋅ THEN Reduce 0 THEN Auto))
   THEN D -1
   ) }

1
1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. ∀as,bs:𝔹 List.  (as ≤ bs ⇒ (t bs) ⇒ (t as))
5. eff-unique(t)
6. ∀n:ℕ
     ∃k:ℕ
      ((n ≤ k)
      ∧ (∀b,c:𝔹 List.
           ((||b|| = k ∈ ℤ) ⇒ (||c|| = k ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
7. a : n:ℕ ⟶ (𝔹 List)
8. ∀n:ℕ. ((||a n|| = n ∈ ℤ) ∧ (t (a n)))
9. k0 : n:ℕ ⟶ ℕ
10. ∀n:ℕ
      ((n ≤ (k0 n))
      ∧ (∀b,c:𝔹 List.
           ((||b|| = (k0 n) ∈ ℤ) ⇒ (||c|| = (k0 n) ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
11. k : ℕ ⟶ ℤ
12. ∀i,j:ℕ.  ((i ≤ j) ⇒ ((k i) ≤ (k j)))
13. ∀n:ℕ. ((k0 n) ≤ (k n))
14. ∀n:ℕ. (n ≤ (k n))
15. ∀n:ℕ. (0 ≤ (k n))
16. b : ℕ ⟶ (𝔹 List)
17. ∀n:ℕ. ((b n) = firstn(n;a (k n)) ∈ (𝔹 List))
⊢ ∃f:ℕ ⟶ 𝔹. is-path(t;f)

---

Latex:

---

Latex:

1.  Fan
2.  t  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}as:\mBbbB{}  List.  Dec(t  as)
4.  \mforall{}as,bs:\mBbbB{}  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (t  bs)  {}\mRightarrow{}  (t  as))
5.  eff-unique(t)
6.  \mforall{}n:\mBbbN{}
          \mexists{}k:\mBbbN{}
            ((n  \mleq{}  k)
            \mwedge{}  (\mforall{}b,c:\mBbbB{}  List.
                      ((||b||  =  k)  {}\mRightarrow{}  (||c||  =  k)  {}\mRightarrow{}  (t  b)  {}\mRightarrow{}  (t  c)  {}\mRightarrow{}  (firstn(n;b)  =  firstn(n;c)))))
7.  a  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  List)
8.  \mforall{}n:\mBbbN{}.  ((||a  n||  =  n)  \mwedge{}  (t  (a  n)))
9.  k0  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
10.  \mforall{}n:\mBbbN{}
            ((n  \mleq{}  (k0  n))
            \mwedge{}  (\mforall{}b,c:\mBbbB{}  List.
                      ((||b||  =  (k0  n))  {}\mRightarrow{}  (||c||  =  (k0  n))  {}\mRightarrow{}  (t  b)  {}\mRightarrow{}  (t  c)  {}\mRightarrow{}  (firstn(n;b)  =  firstn(n;c)))))
11.  k  :  \mBbbN{}  {}\mrightarrow{}  \mBbbZ{}
12.  \mforall{}i,j:\mBbbN{}.    ((i  \mleq{}  j)  {}\mRightarrow{}  ((k  i)  \mleq{}  (k  j)))
13.  \mforall{}n:\mBbbN{}.  ((k0  n)  \mleq{}  (k  n))
14.  \mforall{}n:\mBbbN{}.  (n  \mleq{}  (k  n))
15.  \mforall{}n:\mBbbN{}.  (0  \mleq{}  (k  n))
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  is-path(t;f)


By

---

Latex:
((Assert  \mkleeneopen{}\mexists{}b:\mBbbN{}  {}\mrightarrow{}  (\mBbbB{}  List).  \mforall{}n:\mBbbN{}.  ((b  n)  =  firstn(n;a  (k  n)))\mkleeneclose{}  BY
                (With  \mkleeneopen{}\mlambda{}n.firstn(n;a  (k  n))\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto))
  THEN  D  -1
  )

---

Home Index