---

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

.....antecedent..... 
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. eff-unique-path(T;A)
10. finite-type(T) ⇐ ∃L:T List. ∀x:T. (x ∈ L)
11. L : T List
12. ∀x:T. (x ∈ L)
⊢ ¬↑null(L)
BY
{ (DVar `L'
   THEN Reduce 0
   THEN Auto
   THEN RenameVar `t' (-4)
   THEN With ⌜t⌝ (D (-1))⋅
   THEN Auto
   THEN RWO "nil_member" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
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
9.  eff-unique-path(T;A)
10.  finite-type(T)  \mLeftarrow{}{}  \mexists{}L:T  List.  \mforall{}x:T.  (x  \mmember{}  L)
11.  L  :  T  List
12.  \mforall{}x:T.  (x  \mmember{}  L)
\mvdash{}  \mneg{}\muparrow{}null(L)


By

---

Latex:
(DVar  `L'
  THEN  Reduce  0
  THEN  Auto
  THEN  RenameVar  `t'  (-4)
  THEN  With  \mkleeneopen{}t\mkleeneclose{}  (D  (-1))\mcdot{}
  THEN  Auto
  THEN  RWO  "nil\_member"  (-1)
  THEN  Auto)

---

Home Index