Step
*
of Lemma
bounded-ccc-nset-decidable
∀K:Type. (CCCNSet(K)
⇒ (∀B:ℕ. ((∀k:K. (k ≤ B))
⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))))))
BY
{ (InstLemma `ccc-nset-weakly-decidable` []
THEN RepeatFor 2 ((ParallelLast' THENA Auto))
THEN (InstLemma `ccc-nset-minimum` [⌜K⌝]⋅ THENA Auto)) }
1
1. K : Type
2. CCCNSet(K)
3. WD(K)
4. ∃n:K. ∀m:K. (n ≤ m)
⊢ ∀B:ℕ. ((∀k:K. (k ≤ B))
⇒ (∀l:ℕ. ((l ∈ K) ∨ (¬(l ∈ K)))))
Latex:
Latex:
\mforall{}K:Type. (CCCNSet(K) {}\mRightarrow{} (\mforall{}B:\mBbbN{}. ((\mforall{}k:K. (k \mleq{} B)) {}\mRightarrow{} (\mforall{}l:\mBbbN{}. ((l \mmember{} K) \mvee{} (\mneg{}(l \mmember{} K)))))))
By
Latex:
(InstLemma `ccc-nset-weakly-decidable` []
THEN RepeatFor 2 ((ParallelLast' THENA Auto))
THEN (InstLemma `ccc-nset-minimum` [\mkleeneopen{}K\mkleeneclose{}]\mcdot{} THENA Auto))
Home
Index