---

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

.....assertion..... 
1. K : Type
2. CCCNSet(K)
⊢ ∀d:ℕ. ∀K:Type.  (CCCNSet(K) ⇒ (∀m,k:K.  (k - m < d ⇒ (∀j:K. (m ≤ j)) ⇒ (∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K)))))))
BY
{ ((RepeatFor 2 (Thin (-1)) THEN Unfold `ccc-nset` 0) THEN At ⌜𝕌'⌝CompleteInductionOnNat⋅ THEN (UnivCD THENA Auto)) }

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

---

Latex:

---

Latex:
.....assertion..... 
1.  K  :  Type
2.  CCCNSet(K)
\mvdash{}  \mforall{}d:\mBbbN{}.  \mforall{}K:Type.
        (CCCNSet(K)
        {}\mRightarrow{}  (\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)))))))


By

---

Latex:
((RepeatFor  2  (Thin  (-1))  THEN  Unfold  `ccc-nset`  0)
  THEN  At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}CompleteInductionOnNat\mcdot{}
  THEN  (UnivCD  THENA  Auto))

---

Home Index