---

Step * 1 of Lemma unbounded-ccc-nset-decidable


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))
BY
{ ((Decide ⌜n ≤ l⌝⋅ THENA Auto) THENL [BackThruSomeHyp; (OrRight THEN Auto)]) }

---

Latex:

---

Latex:

1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  K
4.  CCC(K)
5.  K  \msubseteq{}r  \mBbbN{}
6.  \mforall{}m,k:K.  \mforall{}l:\{m..k\msupminus{}\}.    ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K)))
7.  n  :  K
8.  \mforall{}m:K.  (n  \mleq{}  m)
9.  \mforall{}B:\mBbbN{}.  \mexists{}k:K.  B  <  k
10.  l  :  \mBbbN{}
11.  k  :  K
12.  l  <  k
13.  \mforall{}l:\{n..k\msupminus{}\}.  ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K)))
\mvdash{}  (l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K))


By

---

Latex:
((Decide  \mkleeneopen{}n  \mleq{}  l\mkleeneclose{}\mcdot{}  THENA  Auto)  THENL  [BackThruSomeHyp;  (OrRight  THEN  Auto)])

---

Home Index