---

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


1. [T] : Type
2. size : ℕ
3. T ~ ℕsize
4. BarSep(T;T)
5. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
6. ¬tbar(T;¬(A))
7. Decidable(A)
8. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
9. T
10. ∀a,b:T.  Dec(a = b ∈ T)
11. eff-unique-path(T;A)
12. u : T
13. u1 : T
14. v : T List
15. ¬False
16. s : T List
17. ∀s:T List
      ∃t:{t:T| (t ∈ [u1 / v])} . ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
18. t : {t:T| (t ∈ [u1 / v])} 
19. ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
⊢ ∃t:{t:T| (t ∈ [u; [u1 / v]])} . ∀t':{t:T| (t ∈ [u; [u1 / v]])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))\000C))
BY
{ (Decide u = t ∈ T THENA Auto) }

1
1. [T] : Type
2. size : ℕ
3. T ~ ℕsize
4. BarSep(T;T)
5. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
6. ¬tbar(T;¬(A))
7. Decidable(A)
8. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
9. T
10. ∀a,b:T.  Dec(a = b ∈ T)
11. eff-unique-path(T;A)
12. u : T
13. u1 : T
14. v : T List
15. ¬False
16. s : T List
17. ∀s:T List
      ∃t:{t:T| (t ∈ [u1 / v])} . ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
18. t : {t:T| (t ∈ [u1 / v])} 
19. ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
20. u = t ∈ T
⊢ ∃t:{t:T| (t ∈ [u; [u1 / v]])} . ∀t':{t:T| (t ∈ [u; [u1 / v]])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))\000C))

2
1. [T] : Type
2. size : ℕ
3. T ~ ℕsize
4. BarSep(T;T)
5. A : {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)} 
6. ¬tbar(T;¬(A))
7. Decidable(A)
8. ∀as,bs:T List.  (as ≤ bs ⇒ (A bs) ⇒ (A as))
9. T
10. ∀a,b:T.  Dec(a = b ∈ T)
11. eff-unique-path(T;A)
12. u : T
13. u1 : T
14. v : T List
15. ¬False
16. s : T List
17. ∀s:T List
      ∃t:{t:T| (t ∈ [u1 / v])} . ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
18. t : {t:T| (t ∈ [u1 / v])} 
19. ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))))
20. ¬(u = t ∈ T)
⊢ ∃t:{t:T| (t ∈ [u; [u1 / v]])} . ∀t':{t:T| (t ∈ [u; [u1 / v]])} . ((¬(t' = t ∈ T)) ⇒ tbar(T;¬(λx.(A ((s @ [t']) @ x)))\000C))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  size  :  \mBbbN{}
3.  T  \msim{}  \mBbbN{}size
4.  BarSep(T;T)
5.  A  :  \{A:(T  List)  {}\mrightarrow{}  \mBbbP{}|  down-closed(T;A)  \mwedge{}  Unbounded(A)\} 
6.  \mneg{}tbar(T;\mneg{}(A))
7.  Decidable(A)
8.  \mforall{}as,bs:T  List.    (as  \mleq{}  bs  {}\mRightarrow{}  (A  bs)  {}\mRightarrow{}  (A  as))
9.  T
10.  \mforall{}a,b:T.    Dec(a  =  b)
11.  eff-unique-path(T;A)
12.  u  :  T
13.  u1  :  T
14.  v  :  T  List
15.  \mneg{}False
16.  s  :  T  List
17.  \mforall{}s:T  List
            \mexists{}t:\{t:T|  (t  \mmember{}  [u1  /  v])\} 
              \mforall{}t':\{t:T|  (t  \mmember{}  [u1  /  v])\}  .  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))
18.  t  :  \{t:T|  (t  \mmember{}  [u1  /  v])\} 
19.  \mforall{}t':\{t:T|  (t  \mmember{}  [u1  /  v])\}  .  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))
\mvdash{}  \mexists{}t:\{t:T|  (t  \mmember{}  [u;  [u1  /  v]])\} 
      \mforall{}t':\{t:T|  (t  \mmember{}  [u;  [u1  /  v]])\}  .  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  tbar(T;\mneg{}(\mlambda{}x.(A  ((s  @  [t'])  @  x)))))


By

---

Latex:
(Decide  u  =  t  THENA  Auto)

---

Home Index