---

Step * 2 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))
⊢ eff-unique-path(T;A) ⇒ (∃f:ℕ ⟶ T [is-path(A;f)])
BY
{ (Assert T BY
         (D 2
          THEN D 3
          THEN D 4
          THEN (With ⌜0⌝ (D 5)⋅ THEN ExRepD)
          THEN Auto
          THEN DVar `A'
          THEN Auto
          THEN With ⌜1⌝ (D (-4))⋅
          THEN Auto
          THEN ExRepD
          THEN D (-3)
          THEN All Reduce 
          THEN Auto
          THEN (Assert f u ∈ ℕsize BY
                      Auto)
          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
⊢ 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))
\mvdash{}  eff-unique-path(T;A)  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T  [is-path(A;f)])


By

---

Latex:
(Assert  T  BY
              (D  2
                THEN  D  3
                THEN  D  4
                THEN  (With  \mkleeneopen{}0\mkleeneclose{}  (D  5)\mcdot{}  THEN  ExRepD)
                THEN  Auto
                THEN  DVar  `A'
                THEN  Auto
                THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  (-4))\mcdot{}
                THEN  Auto
                THEN  ExRepD
                THEN  D  (-3)
                THEN  All  Reduce 
                THEN  Auto
                THEN  (Assert  f  u  \mmember{}  \mBbbN{}size  BY
                                        Auto)
                THEN  Auto'))

---

Home Index