---

Step * 2 2 1 1 1 1 of Lemma ccc-nset-weakly-decidable


1. K : Type
2. K ⊆r ℕ
3. K ∧ CCC(K)
4. ∀d:ℕ. ∀m,k:K.  (k - m < d ⇒ (∀j:K. (m ≤ j)) ⇒ (∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K)))))
5. n : K
6. ∀m:K. (n ≤ m)
7. ∀k:K. ∀l:{n..k-}.  ((l ∈ K) ∨ (¬(l ∈ K)))
8. m : K
9. k : K
10. ∀l:{n..k-}. ((l ∈ K) ∨ (¬(l ∈ K)))
11. l : {m..k-}
⊢ (l ∈ K) ∨ (¬(l ∈ K))
BY
{ (Decide ⌜n ≤ l⌝⋅ THENA Auto) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Decide  \mkleeneopen{}n  \mleq{}  l\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index