Step
*
2
2
1
2
1
1
1
of Lemma
twkl!-implies-dfan
1. T : Type
2. k : ℕ
3. T ~ ℕk
4. WKL!(T)
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T. Dec(a = b ∈ T)
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))
BY
{ (UnfoldTopAb 4
THEN InstHyp [⌜λb.((upwd-closure(T;s) b)
⇒ (tree-big(T;upwd-closure(T;s);||b||)
∧ let as = a ||b|| in
b = (as @ map(λi.t;upto(||b|| - ||as||))) ∈ (T List)))⌝] 4⋅
)⋅ }
1
.....wf.....
1. T : Type
2. k : ℕ
3. T ~ ℕk
4. ∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)}
(Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T. Dec(a = b ∈ T)
⊢ λb.((upwd-closure(T;s) b)
⇒ (tree-big(T;upwd-closure(T;s);||b||) ∧ let as = a ||b|| in b = (as @ map(λi.t;upto(||b|| - ||as||))) ∈ (T List))\000C)
∈ {A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)}
2
.....antecedent.....
1. T : Type
2. k : ℕ
3. T ~ ℕk
4. ∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)}
(Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T. Dec(a = b ∈ T)
⊢ Decidable(λb.((upwd-closure(T;s) b)
⇒ (tree-big(T;upwd-closure(T;s);||b||)
∧ let as = a ||b|| in
b = (as @ map(λi.t;upto(||b|| - ||as||))) ∈ (T List))))
3
.....antecedent.....
1. T : Type
2. k : ℕ
3. T ~ ℕk
4. ∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)}
(Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T. Dec(a = b ∈ T)
⊢ eff-unique-path(T;λb.((upwd-closure(T;s) b)
⇒ (tree-big(T;upwd-closure(T;s);||b||)
∧ let as = a ||b|| in
b = (as @ map(λi.t;upto(||b|| - ||as||))) ∈ (T List))))
4
1. T : Type
2. k : ℕ
3. T ~ ℕk
4. ∀A:{A:(T List) ⟶ ℙ| down-closed(T;A) ∧ Unbounded(A)}
(Decidable(A) ⇒ eff-unique-path(T;A) ⇒ (∃f:{ℕ ⟶ T| is-path(A;f)}))
5. s : (T List) ⟶ ℙ
6. ∀t:T List. Dec(s t)
7. ∀f:ℕ ⟶ T. ∃n:ℕ. (s map(f;upto(n)))
8. ¬(s [])
9. ∀a,b:ℕ. ((a ≤ b) ⇒ tree-big(T;upwd-closure(T;s);a) ⇒ tree-big(T;upwd-closure(T;s);b))
10. a : {n:ℕ| tree-big(T;upwd-closure(T;s);n)} ⟶ (T List)
11. ∀n:{n:ℕ| tree-big(T;upwd-closure(T;s);n)}
(||a n|| < n ∧ (¬(upwd-closure(T;s) (a n))) ∧ tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. ∀n,m:{n:ℕ| tree-big(T;upwd-closure(T;s);n)} . ((a n) = (a m) ∈ (T List))
13. ¬(k = 0 ∈ ℤ)
14. t : T
15. Decidable(upwd-closure(T;s))
16. ∀n:ℕ. Dec(tree-big(T;upwd-closure(T;s);n))
17. ∀a,b:T. Dec(a = b ∈ T)
18. ∃f:{ℕ ⟶ T| is-path(λb.((upwd-closure(T;s) b)
⇒ (tree-big(T;upwd-closure(T;s);||b||)
∧ let as = a ||b|| in
b = (as @ map(λi.t;upto(||b|| - ||as||))) ∈ (T List)));f)}
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))
Latex:
Latex:
1. T : Type
2. k : \mBbbN{}
3. T \msim{} \mBbbN{}k
4. WKL!(T)
5. s : (T List) {}\mrightarrow{} \mBbbP{}
6. \mforall{}t:T List. Dec(s t)
7. \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}. (s map(f;upto(n)))
8. \mneg{}(s [])
9. \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))
10. a : \{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\} {}\mrightarrow{} (T List)
11. \mforall{}n:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\}
(||a n|| < n \mwedge{} (\mneg{}(upwd-closure(T;s) (a n))) \mwedge{} tree-big(T;upwd-closure(T;s);||a n|| + 1))
12. \mforall{}n,m:\{n:\mBbbN{}| tree-big(T;upwd-closure(T;s);n)\} . ((a n) = (a m))
13. \mneg{}(k = 0)
14. t : T
15. Decidable(upwd-closure(T;s))
16. \mforall{}n:\mBbbN{}. Dec(tree-big(T;upwd-closure(T;s);n))
17. \mforall{}a,b:T. Dec(a = b)
\mvdash{} \mexists{}k:\mBbbN{}. \mforall{}f:\mBbbN{} {}\mrightarrow{} T. \mexists{}n:\mBbbN{}k. (s map(f;upto(n)))
By
Latex:
(UnfoldTopAb 4
THEN InstHyp [\mkleeneopen{}\mlambda{}b.((upwd-closure(T;s) b)
{}\mRightarrow{} (tree-big(T;upwd-closure(T;s);||b||)
\mwedge{} let as = a ||b|| in
b = (as @ map(\mlambda{}i.t;upto(||b|| - ||as||)))))\mkleeneclose{}] 4\mcdot{}
)\mcdot{}
Home
Index