---

Step * 2 1 1 1 of Lemma twkl!-implies-dfan

.....aux..... 
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:ℕ
     (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:ℕ. ((¬tree-big(T;upwd-closure(T;s);n)) ⇒ (∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) as)))))
11. ∀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))))
12. n : ℕ
13. [%25] : tree-big(T;upwd-closure(T;s);n)
⊢ tree-big(T;upwd-closure(T;s);n)
BY
{ Assert ⌜Dec(tree-big(T;upwd-closure(T;s);n))⌝⋅ }

1
.....assertion..... 
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:ℕ
     (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:ℕ. ((¬tree-big(T;upwd-closure(T;s);n)) ⇒ (∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) as)))))
11. ∀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))))
12. n : ℕ
13. [%25] : tree-big(T;upwd-closure(T;s);n)
⊢ Dec(tree-big(T;upwd-closure(T;s);n))

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:ℕ
     (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:ℕ. ((¬tree-big(T;upwd-closure(T;s);n)) ⇒ (∃as:T List. ((||as|| = n ∈ ℤ) ∧ (¬(upwd-closure(T;s) as)))))
11. ∀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))))
12. n : ℕ
13. [%25] : tree-big(T;upwd-closure(T;s);n)
14. Dec(tree-big(T;upwd-closure(T;s);n))
⊢ tree-big(T;upwd-closure(T;s);n)

---

Latex:

---

Latex:
.....aux..... 
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:\mBbbN{}
          (tree-big(T;upwd-closure(T;s);n)
          {}\mRightarrow{}  (\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:\mBbbN{}
            ((\mneg{}tree-big(T;upwd-closure(T;s);n))
            {}\mRightarrow{}  (\mexists{}as:T  List.  ((||as||  =  n)  \mwedge{}  (\mneg{}(upwd-closure(T;s)  as)))))
11.  \mforall{}n:\mBbbN{}
            (tree-big(T;upwd-closure(T;s);n)
            {}\mRightarrow{}  (\mexists{}k:\mBbbN{}n.  ((\mneg{}tree-big(T;upwd-closure(T;s);k))  \mwedge{}  tree-big(T;upwd-closure(T;s);k  +  1))))
12.  n  :  \mBbbN{}
13.  [\%25]  :  tree-big(T;upwd-closure(T;s);n)
\mvdash{}  tree-big(T;upwd-closure(T;s);n)


By

---

Latex:
Assert  \mkleeneopen{}Dec(tree-big(T;upwd-closure(T;s);n))\mkleeneclose{}\mcdot{}

---

Home Index