---

Step * 1 2 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)))
⊢ ∃f:ℕ ⟶ 𝔹. is-path(t;f)
BY
{ ((Skolemize (-3) `k0' THENA Auto)
   THEN (InstLemma `monotone-upper-bound-function` [⌜k0⌝]⋅ THENA Auto)
   THEN D -1
   THEN RenameVar `k' (-2)
   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))
⊢ ∃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)))
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  is-path(t;f)


By

---

Latex:
((Skolemize  (-3)  `k0'  THENA  Auto)
  THEN  (InstLemma  `monotone-upper-bound-function`  [\mkleeneopen{}k0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  RenameVar  `k'  (-2)
  THEN  D  -1)

---

Home Index