---

Step * 2 1 1 1 1 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
9. ∀a,b:T.  Dec(a = b ∈ T)
10. eff-unique-path(T;A)
11. u : T
12. (¬↑null([]))
⇒ (∀s:T List. ∃t:{t:T| (t ∈ [])} . ∀t':{t:T| (t ∈ [])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x))))))
13. ¬False
14. s : T List
⊢ ∃t:{t:T| (t ∈ [u])} . ∀t':{t:T| (t ∈ [u])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
BY
{ (With ⌜u⌝ (D 0)⋅ THEN Auto THEN D -1 THEN D (-1)) }

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)
10. eff-unique-path(T;A)
11. u : T
12. (¬↑null([]))
⇒ (∀s:T List. ∃t:{t:T| (t ∈ [])} . ∀t':{t:T| (t ∈ [])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x))))))
13. ¬False
14. s : T List
15. t' : T
16. (t' ∈ [u])
⊢ t' = u ∈ T

---

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
9.  \mforall{}a,b:T.    Dec(a  =  b)
10.  eff-unique-path(T;A)
11.  u  :  T
12.  (\mneg{}\muparrow{}null([]))
{}\mRightarrow{}  (\mforall{}s:T  List
            \mexists{}t:\{t:T|  (t  \mmember{}  [])\}  .  \mforall{}t':\{t:T|  (t  \mmember{}  [])\}  .  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))\000C)
13.  \mneg{}False
14.  s  :  T  List
\mvdash{}  \mexists{}t:\{t:T|  (t  \mmember{}  [u])\}  .  \mforall{}t':\{t:T|  (t  \mmember{}  [u])\}  .  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))


By

---

Latex:
(With  \mkleeneopen{}u\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  D  -1  THEN  D  (-1))

---

Home Index