---

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


1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T)
4. ∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))
5. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
6. Decidable(A)
7. ¬tbar(T;¬(A))
⊢ eff-unique-path(T;A) ⇒ (∃f:ℕ ⟶ T [is-path(A;f)])
BY
{ (Thin 4
   THEN PromoteHyp (-1) 5
   THEN (Assert ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as)) BY
               (RepUR ``dec-predicate`` -1
                THEN DVar `A'
                THEN (Unhide THENA Auto)
                THEN RepUR ``down-closed R-closed`` (-3)
                THEN D -3
                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))
⊢ 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.  \mforall{}A:(T  List)  {}\mrightarrow{}  \mBbbP{}.  (dbar(T;A)  {}\mRightarrow{}  (\mneg{}(down-closed(T;\mneg{}(A))  \mwedge{}  Unbounded(\mneg{}(A)))))
5.  A  :  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
6.  Decidable(A)
7.  \mneg{}tbar(T;\mneg{}(A))
\mvdash{}  eff-unique-path(T;A)  {}\mRightarrow{}  (\mexists{}f:\mBbbN{}  {}\mrightarrow{}  T  [is-path(A;f)])


By

---

Latex:
(Thin  4
  THEN  PromoteHyp  (-1)  5
  THEN  (Assert  \mforall{}as,bs:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (A  bs)  {}\mRightarrow{}  (A  as))  BY
                          (RepUR  ``dec-predicate``  -1
                            THEN  DVar  `A'
                            THEN  (Unhide  THENA  Auto)
                            THEN  RepUR  ``down-closed  R-closed``  (-3)
                            THEN  D  -3
                            THEN  Auto)))

---

Home Index