---

Step * of Lemma CCC-omni

∀K:Type. (CCCNSet(K) ⇒ (∀P:K ⟶ ℙ. ((∀k:K. Dec(P[k])) ⇒ ((∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))))))
BY
{ (Auto
   THEN (InstLemma `ccc-nset-weakly-decidable` [⌜K⌝]⋅ THENA Auto)
   THEN (InstLemma `ccc-nset-minimum` [⌜K⌝]⋅ THENA Auto)
   THEN (Assert ∀n:K. ∀k:ℕn + 1.  Dec(k ∈ K) BY
               (D 2
                THEN Intros
                THEN ExRepD
                THEN D 7
                THEN (InstHyp [⌜n1⌝;⌜n⌝] 8⋅ THENA Auto)
                THEN Fold `decidable` (-1)
                THEN ((Decide ⌜n1 ≤ k⌝⋅ THENA Auto)
                      THENL [((Decide ⌜k < n⌝⋅ THENA Auto)
                              THENL [BackThruSomeHyp
                                    ; ((Assert k = n ∈ ℤ BY Auto) THEN HypSubst' (-1) 0 THEN OrLeft THEN Auto)]
                            )
                            ; (OrRight 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)
⊢ (∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))

---

Latex:

---

Latex:
\mforall{}K:Type.  (CCCNSet(K)  {}\mRightarrow{}  (\mforall{}P:K  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}k:K.  Dec(P[k]))  {}\mRightarrow{}  ((\mexists{}k:K.  P[k])  \mvee{}  (\mforall{}k:K.  (\mneg{}P[k]))))))


By

---

Latex:
(Auto
  THEN  (InstLemma  `ccc-nset-weakly-decidable`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `ccc-nset-minimum`  [\mkleeneopen{}K\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  \mforall{}n:K.  \mforall{}k:\mBbbN{}n  +  1.    Dec(k  \mmember{}  K)  BY
                          (D  2
                            THEN  Intros
                            THEN  ExRepD
                            THEN  D  7
                            THEN  (InstHyp  [\mkleeneopen{}n1\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]  8\mcdot{}  THENA  Auto)
                            THEN  Fold  `decidable`  (-1)
                            THEN  ((Decide  \mkleeneopen{}n1  \mleq{}  k\mkleeneclose{}\mcdot{}  THENA  Auto)
                                        THENL  [((Decide  \mkleeneopen{}k  <  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                        THENL  [BackThruSomeHyp
                                                                    ;  ((Assert  k  =  n  BY
                                                                                        Auto)
                                                                          THEN  HypSubst'  (-1)  0
                                                                          THEN  OrLeft
                                                                          THEN  Auto)]
                                                    )
                                                    ;  (OrRight  THEN  Auto)]
                            ))))

---

Home Index