Step
*
2
2
1
2
1
1
1
3
of Lemma
twkl!-implies-dfan
.....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))))
BY
{ (D 0
THEN Reduce 0
THEN Auto
THEN Assert ⌜∃m:ℕ. (n < m ∧ (upwd-closure(T;s) map(g;upto(m))) ∧ (upwd-closure(T;s) map(h;upto(m))))⌝⋅) }
1
.....assertion.....
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. g : ℕ ⟶ T
19. h : ℕ ⟶ T
20. n : ℕ
21. ¬((g n) = (h n) ∈ T)
⊢ ∃m:ℕ. (n < m ∧ (upwd-closure(T;s) map(g;upto(m))) ∧ (upwd-closure(T;s) map(h;upto(m))))
2
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. g : ℕ ⟶ T
19. h : ℕ ⟶ T
20. n : ℕ
21. ¬((g n) = (h n) ∈ T)
22. ∃m:ℕ. (n < m ∧ (upwd-closure(T;s) map(g;upto(m))) ∧ (upwd-closure(T;s) map(h;upto(m))))
⊢ ∃m:ℕ
(¬(((upwd-closure(T;s) map(g;upto(m)))
⇒ (tree-big(T;upwd-closure(T;s);||map(g;upto(m))||)
∧ let as = a ||map(g;upto(m))|| in
map(g;upto(m)) = (as @ map(λi.t;upto(||map(g;upto(m))|| - ||as||))) ∈ (T List)))
∧ ((upwd-closure(T;s) map(h;upto(m)))
⇒ (tree-big(T;upwd-closure(T;s);||map(h;upto(m))||)
∧ let as = a ||map(h;upto(m))|| in
map(h;upto(m)) = (as @ map(λi.t;upto(||map(h;upto(m))|| - ||as||))) ∈ (T List)))))
Latex:
Latex:
.....antecedent.....
1. T : Type
2. k : \mBbbN{}
3. T \msim{} \mBbbN{}k
4. \mforall{}A:\{A:(T List) {}\mrightarrow{} \mBbbP{}| down-closed(T;A) \mwedge{} Unbounded(A)\}
(Decidable(A) {}\mRightarrow{} eff-unique-path(T;A) {}\mRightarrow{} (\mexists{}f:\{\mBbbN{} {}\mrightarrow{} T| is-path(A;f)\}))
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{} eff-unique-path(T;\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||))))))
By
Latex:
(D 0
THEN Reduce 0
THEN Auto
THEN Assert \mkleeneopen{}\mexists{}m:\mBbbN{}
(n < m \mwedge{} (upwd-closure(T;s) map(g;upto(m))) \mwedge{} (upwd-closure(T;s) map(h;upto(m))))\mkleeneclose{}\mcdot{})
Home
Index