---

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


1. K : Type
2. CCCNSet(K)
3. ∀d:ℕ. ∀K:Type.  (CCCNSet(K) ⇒ (∀m,k:K.  (k - m < d ⇒ (∀j:K. (m ≤ j)) ⇒ (∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K)))))))
⊢ ∀m,k:K. ∀l:{m..k-}.  ((l ∈ K) ∨ (¬(l ∈ K)))
BY
{ ((Assert ∀d:ℕ. ∀m,k:K.  (k - m < d ⇒ (∀j:K. (m ≤ j)) ⇒ (∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K))))) BY
          (ParallelLast THEN (D -1 With ⌜K⌝  THENA Auto) THEN D -1 THEN Auto))
   THEN Thin 3
   THEN skip{(D 2 THEN (UnivCD THENA Auto) THEN InstHyp [⌜1 + (k - m)⌝;⌜m⌝;⌜k⌝;⌜l⌝] 4⋅ THEN Auto)}) }

1
1. K : Type
2. CCCNSet(K)
3. ∀d:ℕ. ∀m,k:K.  (k - m < d ⇒ (∀j:K. (m ≤ j)) ⇒ (∀l:{m..k-}. ((l ∈ K) ∨ (¬(l ∈ K)))))
⊢ ∀m,k:K. ∀l:{m..k-}.  ((l ∈ K) ∨ (¬(l ∈ K)))

---

Latex:

---

Latex:

1.  K  :  Type
2.  CCCNSet(K)
3.  \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)))))))
\mvdash{}  \mforall{}m,k:K.  \mforall{}l:\{m..k\msupminus{}\}.    ((l  \mmember{}  K)  \mvee{}  (\mneg{}(l  \mmember{}  K)))


By

---

Latex:
((Assert  \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)))))  BY
                (ParallelLast  THEN  (D  -1  With  \mkleeneopen{}K\mkleeneclose{}    THENA  Auto)  THEN  D  -1  THEN  Auto))
  THEN  Thin  3
  THEN  skip\{(D  2  THEN  (UnivCD  THENA  Auto)  THEN  InstHyp  [\mkleeneopen{}1  +  (k  -  m)\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]  4\mcdot{}  THEN  Auto)\})

---

Home Index