---

Step * 1 of Lemma CCC-omni


1. K : Type
2. CCCNSet(K)
3. P : K ⟶ ℙ
4. ∀k:K. Dec(P[k])
5. WD(K)
6. ∃n:K. ∀m:K. (n ≤ m)
7. ∀n:K. ∀k:ℕn + 1.  Dec(k ∈ K)
⊢ (∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))
BY
{ ((Assert ∀n:K. Dec(∃k:K. ((k ≤ n) ∧ P[k])) BY
          ((D 0 THENA Auto)
           THEN (Assert ⌜Dec(∃k:ℕn + 1. ((k ∈ K) ∧ P[k]))⌝⋅
           THENM ((D 2 THEN RepeatFor 3 (ParallelLast)) THENL [Auto; (ExRepD THEN D 0 With ⌜k⌝  THEN Auto)])
           )
           THEN D 2
           THEN Auto))
   THEN (Assert ∀n:K. Dec(∀k:K. ((k ≤ n) ⇒ (¬P[k]))) BY
               ((D 0 THENA Auto)
                THEN (Assert ⌜Dec(∀k:ℕn + 1. ((k ∈ K) ⇒ (¬P[k])))⌝⋅
                THENM (D 2 THEN RepeatFor 2 (ParallelLast) THEN Try (ParallelNot (-1)) THEN Auto)
                )
                THEN D 2
                THEN Auto))
   ) }

1
1. K : Type
2. CCCNSet(K)
3. P : K ⟶ ℙ
4. ∀k:K. Dec(P[k])
5. WD(K)
6. ∃n:K. ∀m:K. (n ≤ m)
7. ∀n:K. ∀k:ℕn + 1.  Dec(k ∈ K)
8. ∀n:K. Dec(∃k:K. ((k ≤ n) ∧ P[k]))
9. ∀n:K. Dec(∀k:K. ((k ≤ n) ⇒ (¬P[k])))
⊢ (∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))

---

Latex:

---

Latex:

1.  K  :  Type
2.  CCCNSet(K)
3.  P  :  K  {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}k:K.  Dec(P[k])
5.  WD(K)
6.  \mexists{}n:K.  \mforall{}m:K.  (n  \mleq{}  m)
7.  \mforall{}n:K.  \mforall{}k:\mBbbN{}n  +  1.    Dec(k  \mmember{}  K)
\mvdash{}  (\mexists{}k:K.  P[k])  \mvee{}  (\mforall{}k:K.  (\mneg{}P[k]))


By

---

Latex:
((Assert  \mforall{}n:K.  Dec(\mexists{}k:K.  ((k  \mleq{}  n)  \mwedge{}  P[k]))  BY
                ((D  0  THENA  Auto)
                  THEN  (Assert  \mkleeneopen{}Dec(\mexists{}k:\mBbbN{}n  +  1.  ((k  \mmember{}  K)  \mwedge{}  P[k]))\mkleeneclose{}\mcdot{}
                  THENM  ((D  2  THEN  RepeatFor  3  (ParallelLast))
                                THENL  [Auto;  (ExRepD  THEN  D  0  With  \mkleeneopen{}k\mkleeneclose{}    THEN  Auto)]
                              )
                  )
                  THEN  D  2
                  THEN  Auto))
  THEN  (Assert  \mforall{}n:K.  Dec(\mforall{}k:K.  ((k  \mleq{}  n)  {}\mRightarrow{}  (\mneg{}P[k])))  BY
                          ((D  0  THENA  Auto)
                            THEN  (Assert  \mkleeneopen{}Dec(\mforall{}k:\mBbbN{}n  +  1.  ((k  \mmember{}  K)  {}\mRightarrow{}  (\mneg{}P[k])))\mkleeneclose{}\mcdot{}
                            THENM  (D  2  THEN  RepeatFor  2  (ParallelLast)  THEN  Try  (ParallelNot  (-1))  THEN  Auto)
                            )
                            THEN  D  2
                            THEN  Auto))
  )

---

Home Index