---

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


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)
BY
{ (Unfold `PFan` (-1)
   THEN RenameVar `t' 2
   THEN Assert ⌜∀n:ℕ
                  ∃k:ℕ
                   ((n ≤ k)
                   ∧ (∀b,c:𝔹 List.
                        ((||b|| = k ∈ ℤ)
                        ⇒ (||c|| = k ∈ ℤ)
                        ⇒ (t b)
                        ⇒ (t c)
                        ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))⌝⋅) }

1
.....assertion..... 
1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. ∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
     ((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
     ⇒ (∀bc,bc':(𝔹 × 𝔹) List.  (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
     ⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
           ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
           ⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
     ⇒ (∃k:ℕ
          ∀gh:ℕ ⟶ (𝔹 × 𝔹)
            ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
⊢ ∀n:ℕ
    ∃k:ℕ
     ((n ≤ k)
     ∧ (∀b,c:𝔹 List.  ((||b|| = k ∈ ℤ) ⇒ (||c|| = k ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))

2
1. Fan
2. t : (𝔹 List) ⟶ ℙ
3. ∀as:𝔹 List. Dec(t as)
4. infinite-tree(t)
5. eff-unique(t)
6. ∀n:ℕ. ∀ss:((𝔹 × 𝔹) List) ⟶ ℙ.
     ((∀bc:(𝔹 × 𝔹) List. Dec(ss bc))
     ⇒ (∀bc,bc':(𝔹 × 𝔹) List.  (bc ≤ bc' ⇒ (ss bc) ⇒ (ss bc')))
     ⇒ (∀gh:ℕ ⟶ (𝔹 × 𝔹)
           ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List)))
           ⇒ (∃m:ℕ. (ss map(gh;upto(m))))))
     ⇒ (∃k:ℕ
          ∀gh:ℕ ⟶ (𝔹 × 𝔹)
            ((¬(map(λi.(fst((gh i)));upto(n)) = map(λi.(snd((gh i)));upto(n)) ∈ (𝔹 List))) ⇒ (ss map(gh;upto(k))))))
7. ∀n:ℕ
     ∃k:ℕ
      ((n ≤ k)
      ∧ (∀b,c:𝔹 List.
           ((||b|| = k ∈ ℤ) ⇒ (||c|| = k ∈ ℤ) ⇒ (t b) ⇒ (t c) ⇒ (firstn(n;b) = firstn(n;c) ∈ (𝔹 List)))))
⊢ ∃f:ℕ ⟶ 𝔹. is-path(t;f)

---

Latex:

---

Latex:

1.  Fan
2.  A  :  (\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}as:\mBbbB{}  List.  Dec(A  as)
4.  infinite-tree(A)
5.  eff-unique(A)
6.  PFan\{i:l\}()
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  is-path(A;f)


By

---

Latex:
(Unfold  `PFan`  (-1)
  THEN  RenameVar  `t'  2
  THEN  Assert  \mkleeneopen{}\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)))))\mkleeneclose{}\mcdot{})

---

Home Index