Step
*
2
1
1
2
1
2
of Lemma
twkl!-implies-dfan
1. T : Type
2. ∃k:ℕ. T ~ ℕk
3. WKL!(T)
4. s : (T List) ⟶ ℙ
5. ∀t:T List. Dec(s t)
6. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
7. ¬(s [])
8. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
9. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
∃k:ℕn. ((¬tree-big(T;upwd-closure(T;s);k)) ∧ tree-big(T;upwd-closure(T;s);k + 1))
10. ∀n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} . ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) as)))
11. nb : n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ ℕn
12. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
((¬tree-big(T;upwd-closure(T;s);nb n)) ∧ tree-big(T;upwd-closure(T;s);(nb n) + 1))
13. u : n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
14. ∀n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} . ((||u n|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) (u n))))
⊢ (∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||u (nb n)|| < n ∧ (¬(upwd-closure(T;s) (u (nb n)))) ∧ tree-big(T;upwd-closure(T;s);||u (nb n)|| + 1)))
∧ (∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((u (nb n)) = (u (nb m)) ∈ (T List)))
BY
{ BetterSplitAndConcl }
1
1. T : Type
2. ∃k:ℕ. T ~ ℕk
3. WKL!(T)
4. s : (T List) ⟶ ℙ
5. ∀t:T List. Dec(s t)
6. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
7. ¬(s [])
8. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
9. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
∃k:ℕn. ((¬tree-big(T;upwd-closure(T;s);k)) ∧ tree-big(T;upwd-closure(T;s);k + 1))
10. ∀n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} . ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) as)))
11. nb : n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ ℕn
12. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
((¬tree-big(T;upwd-closure(T;s);nb n)) ∧ tree-big(T;upwd-closure(T;s);(nb n) + 1))
13. u : n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
14. ∀n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} . ((||u n|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) (u n))))
⊢ ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||u (nb n)|| < n ∧ (¬(upwd-closure(T;s) (u (nb n)))) ∧ tree-big(T;upwd-closure(T;s);||u (nb n)|| + 1))
2
1. T : Type
2. ∃k:ℕ. T ~ ℕk
3. WKL!(T)
4. s : (T List) ⟶ ℙ
5. ∀t:T List. Dec(s t)
6. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
7. ¬(s [])
8. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
9. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
∃k:ℕn. ((¬tree-big(T;upwd-closure(T;s);k)) ∧ tree-big(T;upwd-closure(T;s);k + 1))
10. ∀n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} . ∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) as)))
11. nb : n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ ℕn
12. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
((¬tree-big(T;upwd-closure(T;s);nb n)) ∧ tree-big(T;upwd-closure(T;s);(nb n) + 1))
13. u : n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
14. ∀n:{n:ℕ| ¬tree-big(T;upwd-closure(T;s);n)} . ((||u n|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) (u n))))
15. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||u (nb n)|| < n ∧ (¬(upwd-closure(T;s) (u (nb n)))) ∧ tree-big(T;upwd-closure(T;s);||u (nb n)|| + 1))
⊢ ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((u (nb n)) = (u (nb m)) ∈ (T List))
Latex:
Latex:
1. T : Type
2. \mexists{}k:\mBbbN{}. T \msim{} \mBbbN{}k
3. WKL!(T)
4. s : (T List) {}\mrightarrow{} \mBbbP{}
5. \mforall{}t:T List. Dec(s t)
6. \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}. (s map(f;upto(n)))
7. \mneg{}(s [])
8. \mforall{}a,b:\mBbbN{}. ((a \mleq{} b) {}\mRightarrow{} tree-big(T;upwd-closure(T;s);a) {}\mRightarrow{} tree-big(T;upwd-closure(T;s);b))
9. \mforall{}n:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\}
\mexists{}k:\mBbbN{}n. ((\mneg{}tree-big(T;upwd-closure(T;s);k)) \mwedge{} tree-big(T;upwd-closure(T;s);k + 1))
10. \mforall{}n:\{n:\mBbbN{}| \mneg{}tree-big(T;upwd-closure(T;s);n)\}
\mexists{}as:T List. ((||as|| = n) \mwedge{} (\mneg{}(upwd-closure(T;s) as)))
11. nb : n:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\} {}\mrightarrow{} \mBbbN{}n
12. \mforall{}n:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\}
((\mneg{}tree-big(T;upwd-closure(T;s);nb n)) \mwedge{} tree-big(T;upwd-closure(T;s);(nb n) + 1))
13. u : n:\{n:\mBbbN{}| \mneg{}tree-big(T;upwd-closure(T;s);n)\} {}\mrightarrow{} (T List)
14. \mforall{}n:\{n:\mBbbN{}| \mneg{}tree-big(T;upwd-closure(T;s);n)\} . ((||u n|| = n) \mwedge{} (\mneg{}(upwd-closure(T;s) (u n))))
\mvdash{} (\mforall{}n:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\}
(||u (nb n)|| < n
\mwedge{} (\mneg{}(upwd-closure(T;s) (u (nb n))))
\mwedge{} tree-big(T;upwd-closure(T;s);||u (nb n)|| + 1)))
\mwedge{} (\mforall{}n,m:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\} . ((u (nb n)) = (u (nb m))))
By
Latex:
BetterSplitAndConcl
Home
Index