---

Step * 1 2 of Lemma alt-bar-sep-wkl!


1. [T] : Type
2. BarSep(T;T)
3. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. L : T List
10. ∀x:T. (x ∈ L)
11. ¬↑null(L)
12. ∀n:ℕ. ∀s:ℕn ⟶ T.  ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
⊢ ∃f:ℕ ⟶ T [IsPath(A;f)]
BY
{ (Thin 2 THEN RepeatFor 3 (Thin (-2)) THEN RepeatFor 3 (Thin (-3))) }

1
1. [T] : Type
2. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
3. ¬bar(¬(A))
4. ∀a,b:T.  Dec(a = b ∈ T)
5. ∀n:ℕ. ∀s:ℕn ⟶ T.  ∃t:T. ∀t':T. ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
⊢ ∃f:ℕ ⟶ T [IsPath(A;f)]

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  BarSep(T;T)
3.  A  :  \{A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}|  Tree(A)  \mwedge{}  Unbounded(A)\} 
4.  \mneg{}bar(\mneg{}(A))
5.  AtMostOnePath(A)
6.  Tree(A)
7.  t0  :  T
8.  \mforall{}a,b:T.    Dec(a  =  b)
9.  L  :  T  List
10.  \mforall{}x:T.  (x  \mmember{}  L)
11.  \mneg{}\muparrow{}null(L)
12.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
            \mexists{}t:T.  \mforall{}t':T.  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t';s')))))
\mvdash{}  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  T  [IsPath(A;f)]


By

---

Latex:
(Thin  2  THEN  RepeatFor  3  (Thin  (-2))  THEN  RepeatFor  3  (Thin  (-3)))

---

Home Index