---

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


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-}
10. CCCNSet({k:K| ¬(k = m ∈ ℤ)} )
11. n : {k:K| ¬(k = m ∈ ℤ)} 
12. ∀m:{k:K| ¬(k = m ∈ ℤ)} . (n ≤ m)
13. ∀l:{n..k-}. ((l ∈ {k:K| ¬(k = m ∈ ℤ)} ) ∨ (¬(l ∈ {k:K| ¬(k = m ∈ ℤ)} )))
⊢ (l ∈ K) ∨ (¬(l ∈ K))
BY
{ (Decide ⌜n ≤ l⌝⋅ 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-}
10. CCCNSet({k:K| ¬(k = m ∈ ℤ)} )
11. n : {k:K| ¬(k = m ∈ ℤ)} 
12. ∀m:{k:K| ¬(k = m ∈ ℤ)} . (n ≤ m)
13. ∀l:{n..k-}. ((l ∈ {k:K| ¬(k = m ∈ ℤ)} ) ∨ (¬(l ∈ {k:K| ¬(k = m ∈ ℤ)} )))
14. n ≤ l
⊢ (l ∈ K) ∨ (¬(l ∈ K))

2
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-}
10. CCCNSet({k:K| ¬(k = m ∈ ℤ)} )
11. n : {k:K| ¬(k = m ∈ ℤ)} 
12. ∀m:{k:K| ¬(k = m ∈ ℤ)} . (n ≤ m)
13. ∀l:{n..k-}. ((l ∈ {k:K| ¬(k = m ∈ ℤ)} ) ∨ (¬(l ∈ {k:K| ¬(k = m ∈ ℤ)} )))
14. ¬(n ≤ l)
⊢ (l ∈ K) ∨ (¬(l ∈ K))

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d.  \mforall{}K:Type.
          (((K  \msubseteq{}r  \mBbbN{})  \mwedge{}  K  \mwedge{}  CCC(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)))))))
3.  K  :  Type
4.  (K  \msubseteq{}r  \mBbbN{})  \mwedge{}  K  \mwedge{}  CCC(K)
5.  m  :  K
6.  k  :  K
7.  k  -  m  <  d
8.  \mforall{}j:K.  (m  \mleq{}  j)
9.  l  :  \{m..k\msupminus{}\}
10.  CCCNSet(\{k:K|  \mneg{}(k  =  m)\}  )
11.  n  :  \{k:K|  \mneg{}(k  =  m)\} 
12.  \mforall{}m:\{k:K|  \mneg{}(k  =  m)\}  .  (n  \mleq{}  m)
13.  \mforall{}l:\{n..k\msupminus{}\}.  ((l  \mmember{}  \{k:K|  \mneg{}(k  =  m)\}  )  \mvee{}  (\mneg{}(l  \mmember{}  \{k:K|  \mneg{}(k  =  m)\}  )))
\mvdash{}  (l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K))


By

---

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

---

Home Index