---

Step * 1 of Lemma CCC-omni-2

.....decidable?..... 
1. K : Type
2. CCCNSet(K)
3. ∀P:K ⟶ ℙ. ((∀k:K. Dec(P[k])) ⇒ ((∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))))
4. P : K ⟶ K ⟶ ℙ
5. ∀k,m:K.  Dec(P[k;m])
6. k : K
⊢ Dec(∀m:K. P[k;m])
BY
{ (InstLemma `CCC-omni` [⌜K⌝;⌜λ2m.¬P[k;m]⌝]⋅ THEN Auto THEN D -1) }

1
1. K : Type
2. CCCNSet(K)
3. ∀P:K ⟶ ℙ. ((∀k:K. Dec(P[k])) ⇒ ((∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))))
4. P : K ⟶ K ⟶ ℙ
5. ∀k,m:K.  Dec(P[k;m])
6. k : K
7. ∃k@0:K. (¬P[k;k@0])
⊢ Dec(∀m:K. P[k;m])

2
1. K : Type
2. CCCNSet(K)
3. ∀P:K ⟶ ℙ. ((∀k:K. Dec(P[k])) ⇒ ((∃k:K. P[k]) ∨ (∀k:K. (¬P[k]))))
4. P : K ⟶ K ⟶ ℙ
5. ∀k,m:K.  Dec(P[k;m])
6. k : K
7. ∀k@0:K. (¬¬P[k;k@0])
⊢ Dec(∀m:K. P[k;m])

---

Latex:

---

Latex:
.....decidable?..... 
1.  K  :  Type
2.  CCCNSet(K)
3.  \mforall{}P:K  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}k:K.  Dec(P[k]))  {}\mRightarrow{}  ((\mexists{}k:K.  P[k])  \mvee{}  (\mforall{}k:K.  (\mneg{}P[k]))))
4.  P  :  K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}k,m:K.    Dec(P[k;m])
6.  k  :  K
\mvdash{}  Dec(\mforall{}m:K.  P[k;m])


By

---

Latex:
(InstLemma  `CCC-omni`  [\mkleeneopen{}K\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}m.\mneg{}P[k;m]\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  D  -1)

---

Home Index