---

Step * 2 2 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 ∈ ℤ
⊢ ∃k:ℕ. ∀f:ℕ ⟶ T. ∃n:ℕk. (s map(f;upto(n)))
BY
{ ((With ⌜0⌝ (D 0)⋅ THEN Auto)
   THEN (Assert ⌜T⌝
               ⋅ BY
               (UseWitness ⌜f 0⌝⋅ THEN Auto))
   THEN (Assert ¬T BY
               (BLemma `equipollent-zero` ⋅ THEN Auto))
   THEN Auto) }

---

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


By

---

Latex:
((With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
  THEN  (Assert  \mkleeneopen{}T\mkleeneclose{}
                          \mcdot{}  BY
                          (UseWitness  \mkleeneopen{}f  0\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  \mneg{}T  BY
                          (BLemma  `equipollent-zero`  \mcdot{}  THEN  Auto))
  THEN  Auto)

---

Home Index