---

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


1. [T] : Type
2. BarSep(T;T)
3. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. u : T
10. ¬False
11. n : ℕ
12. s : ℕn ⟶ T
13. t : T
14. ¬(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'))))
BY
{ (RenameVar `m' (-4) THEN (BackThruHyp' 2 THENW Auto) THEN D 0 THEN Reduce 0 THEN Auto) }

1
1. [T] : Type
2. ∀A,B:n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹.  (jbar(A;B) ⇒ (bar(A) ∨ bar(B)))
3. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ 𝔹
4. ¬bar(¬(A))
5. AtMostOnePath(A)
6. Tree(A)
7. t0 : T
8. ∀a,b:T.  Dec(a = b ∈ T)
9. u : T
10. ¬False
11. m : ℕ
12. s : ℕm ⟶ T
13. t : T
14. ¬(u = t ∈ T)
15. f : ℕ ⟶ T
16. g : ℕ ⟶ T
⊢ (∃n:ℕ. (↑(¬(λk,s'. (A ((m + 1) + k) seq-append(m + 1;s.u;s'))) n f)))
∨ (∃n:ℕ. (↑(¬(λk,s'. (A ((m + 1) + k) seq-append(m + 1;s.t;s'))) n g)))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  BarSep(T;T)
3.  A  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbB{}
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.  \mneg{}False
11.  n  :  \mBbbN{}
12.  s  :  \mBbbN{}n  {}\mrightarrow{}  T
13.  t  :  T
14.  \mneg{}(u  =  t)
\mvdash{}  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'))))


By

---

Latex:
(RenameVar  `m'  (-4)  THEN  (BackThruHyp'  2  THENW  Auto)  THEN  D  0  THEN  Reduce  0  THEN  Auto)

---

Home Index