---

Step * 1 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))
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))
BY
{ ((With ⌜1⌝ (D 0)⋅ THEN Auto) THEN With ⌜0⌝ (D 0)⋅ THEN Reduce 0 THEN Auto)⋅ }

---

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.  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))
\mvdash{}  \mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}k.  (s  map(f;upto(n)))


By

---

Latex:
((With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Reduce  0  THEN  Auto)\mcdot{}

---

Home Index