---

Step * 1 1 1 2 1 2 of Lemma alt-bar-sep-wkl!


1. [T] : Type
2. BarSep(T;T)
3. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. u : T
10. u1 : T
11. v : T List
12. ¬False
13. n : ℕ
14. s : ℕn ⟶ T
15. ∀n:ℕ. ∀s:ℕn ⟶ T.
      ∃t:{t:T| (t ∈ [u1 / v])} 
       ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
16. t : {t:T| (t ∈ [u1 / v])} 
17. ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
18. ¬(u = t ∈ T)
⊢ ∃t:{t:T| (t ∈ [u; [u1 / v]])} 
   ∀t':{t:T| (t ∈ [u; [u1 / v]])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
BY
{ Assert ⌜bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.u;s')))) ∨ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t\000C;s'))))⌝
⋅ }

1
.....assertion..... 
1. [T] : Type
2. BarSep(T;T)
3. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. u : T
10. u1 : T
11. v : T List
12. ¬False
13. n : ℕ
14. s : ℕn ⟶ T
15. ∀n:ℕ. ∀s:ℕn ⟶ T.
      ∃t:{t:T| (t ∈ [u1 / v])} 
       ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
16. t : {t:T| (t ∈ [u1 / v])} 
17. ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
18. ¬(u = t ∈ T)
⊢ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.u;s')))) ∨ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t;s'))))

2
1. [T] : Type
2. BarSep(T;T)
3. A : {A:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹| Tree(A) ∧ Unbounded(A)} 
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. u : T
10. u1 : T
11. v : T List
12. ¬False
13. n : ℕ
14. s : ℕn ⟶ T
15. ∀n:ℕ. ∀s:ℕn ⟶ T.
      ∃t:{t:T| (t ∈ [u1 / v])} 
       ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
16. t : {t:T| (t ∈ [u1 / v])} 
17. ∀t':{t:T| (t ∈ [u1 / v])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))
18. ¬(u = t ∈ T)
19. bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.u;s')))) ∨ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t;s')))\000C)
⊢ ∃t:{t:T| (t ∈ [u; [u1 / v]])} 
   ∀t':{t:T| (t ∈ [u; [u1 / v]])} . ((¬(t' = t ∈ T)) ⇒ bar(¬(λk,s'. (A ((n + 1) + k) seq-append(n + 1;s.t';s')))))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  BarSep(T;T)
3.  A  :  \{A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}|  Tree(A)  \mwedge{}  Unbounded(A)\} 
4.  \mneg{}bar(\mneg{}(A))
5.  AtMostOnePath(A)
6.  Tree(A)
7.  t0  :  T
8.  \mforall{}a,b:T.    Dec(a  =  b)
9.  u  :  T
10.  u1  :  T
11.  v  :  T  List
12.  \mneg{}False
13.  n  :  \mBbbN{}
14.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
15.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  T.
            \mexists{}t:\{t:T|  (t  \mmember{}  [u1  /  v])\} 
              \mforall{}t':\{t:T|  (t  \mmember{}  [u1  /  v])\} 
                  ((\mneg{}(t'  =  t))  {}\mRightarrow{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t';s')))))
16.  t  :  \{t:T|  (t  \mmember{}  [u1  /  v])\} 
17.  \mforall{}t':\{t:T|  (t  \mmember{}  [u1  /  v])\} 
            ((\mneg{}(t'  =  t))  {}\mRightarrow{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t';s')))))
18.  \mneg{}(u  =  t)
\mvdash{}  \mexists{}t:\{t:T|  (t  \mmember{}  [u;  [u1  /  v]])\} 
      \mforall{}t':\{t:T|  (t  \mmember{}  [u;  [u1  /  v]])\} 
          ((\mneg{}(t'  =  t))  {}\mRightarrow{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t';s')))))


By

---

Latex:
Assert  \mkleeneopen{}bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.u;s'))))
                \mvee{}  bar(\mneg{}(\mlambda{}k,s'.  (A  ((n  +  1)  +  k)  seq-append(n  +  1;s.t;s'))))\mkleeneclose{}\mcdot{}

---

Home Index