---

Step * 2 1 1 of Lemma bar-separation-implies-twkl!


1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
⊢ eff-unique-path(T;A) ⇒ (∃f:ℕ ⟶ T [is-path(A;f)])
BY
{ (Assert ∀a,b:T.  Dec(a = b ∈ T) BY
         (Auto
          THEN D 2
          THEN D 3
          THEN (Decide ⌜(f a) = (f b) ∈ ℕsize⌝⋅ THENA Auto)
          THEN Try ((OrLeft THEN Complete (Auto)))
          THEN (OrRight THEN Auto)⋅
          THEN ParallelLast
          THEN Auto)) }

1
1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
5. ¬tbar(T;¬(A))
6. Decidable(A)
7. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
8. T
9. ∀a,b:T.  Dec(a = b ∈ T)
⊢ eff-unique-path(T;A) ⇒ (∃f:ℕ ⟶ T [is-path(A;f)])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size
3.  BarSep(T;T)
4.  A  :  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
5.  \mneg{}tbar(T;\mneg{}(A))
6.  Decidable(A)
7.  \mforall{}as,bs:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (A  bs)  {}\mRightarrow{}  (A  as))
8.  T
\mvdash{}  eff-unique-path(T;A)  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T  [is-path(A;f)])


By

---

Latex:
(Assert  \mforall{}a,b:T.    Dec(a  =  b)  BY
              (Auto
                THEN  D  2
                THEN  D  3
                THEN  (Decide  \mkleeneopen{}(f  a)  =  (f  b)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  Try  ((OrLeft  THEN  Complete  (Auto)))
                THEN  (OrRight  THEN  Auto)\mcdot{}
                THEN  ParallelLast
                THEN  Auto))

---

Home Index