---

Step * of Lemma unbounded-ccc-nset-decidable

∀K:Type. (CCCNSet(K) ⇒ (∀B:ℕ. ∃k:K. B < k) ⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))))
BY
{ (InstLemma `ccc-nset-weakly-decidable` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN (InstLemma `ccc-nset-minimum` [⌜K⌝]⋅ THENA Auto)
   THEN D 2
   THEN (D 0 THENA Auto)
   THEN ParallelLast
   THEN ExRepD
   THEN D 5
   THEN (InstHyp [⌜n⌝;⌜k⌝] 6⋅ THENA Auto)) }

1
1. K : Type
2. K ⊆r ℕ
3. K
4. CCC(K)
5. K ⊆r ℕ
6. ∀m,k:K. ∀l:{m..k-}.  ((l ∈ K) ∨ (¬(l ∈ K)))
7. n : K
8. ∀m:K. (n ≤ m)
9. ∀B:ℕ. ∃k:K. B < k
10. l : ℕ
11. k : K
12. l < k
13. ∀l:{n..k-}. ((l ∈ K) ∨ (¬(l ∈ K)))
⊢ (l ∈ K) ∨ (¬(l ∈ K))

---

Latex:

---

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  (\mforall{}B:\mBbbN{}.  \mexists{}k:K.  B  <  k)  {}\mRightarrow{}  (\mforall{}l:\mBbbN{}.  ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K)))))


By

---

Latex:
(InstLemma  `ccc-nset-weakly-decidable`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  (InstLemma  `ccc-nset-minimum`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  2
  THEN  (D  0  THENA  Auto)
  THEN  ParallelLast
  THEN  ExRepD
  THEN  D  5
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]  6\mcdot{}  THENA  Auto))

---

Home Index