---

Step * of Lemma d-CCC-finite

∀[T:Type]. (finite(T) ⇒ dCCC(T))
BY
{ (InstLemma `decidable-exists-finite` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN D 0
   THEN Auto
   THEN (Assert ∀n:ℕ. Dec(∃m:T. (¬↑(R n m))) BY
               Auto)
   THEN RenameVar `d' (-1)
   THEN (Assert T ∨ (¬T) BY
               (BLemma `finite-decidable-inhabited` THEN Auto))
   THEN (D -1 THENL [RenameVar `t' (-1); (D 0 With ⌜0⌝  THEN Auto)])) }

1
1. [T] : Type
2. finite(T)
3. ∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))
4. R : ℕ ⟶ T ⟶ 𝔹
5. ∀g:ℕ ⟶ T. ∃n:ℕ. (↑(R n (g n)))
6. d : ∀n:ℕ. Dec(∃m:T. (¬↑(R n m)))
7. t : T
⊢ ∃n:ℕ. ∀m:T. (↑(R n m))

---

Latex:

---

Latex:
\mforall{}[T:Type].  (finite(T)  {}\mRightarrow{}  dCCC(T))


By

---

Latex:
(InstLemma  `decidable-exists-finite`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  D  0
  THEN  Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}.  Dec(\mexists{}m:T.  (\mneg{}\muparrow{}(R  n  m)))  BY
                          Auto)
  THEN  RenameVar  `d'  (-1)
  THEN  (Assert  T  \mvee{}  (\mneg{}T)  BY
                          (BLemma  `finite-decidable-inhabited`  THEN  Auto))
  THEN  (D  -1  THENL  [RenameVar  `t'  (-1);  (D  0  With  \mkleeneopen{}0\mkleeneclose{}    THEN  Auto)]))

---

Home Index