---

Step * of Lemma CCC-omni-2

∀K:Type
  (CCCNSet(K) ⇒ (∀P:K ⟶ K ⟶ ℙ. ((∀k,m:K.  Dec(P[k;m])) ⇒ ((∃k:K. ∀m:K. P[k;m]) ∨ (∀k:K. (¬(∀m:K. P[k;m])))))))
BY
{ (InstLemma `CCC-omni` [] THEN RepeatFor 2 ((ParallelLast' THENA Auto)) THEN Auto THEN BHyp 3 THEN Auto) }

1
.....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])

---

Latex:

---

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


By

---

Latex:
(InstLemma  `CCC-omni`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  Auto
  THEN  BHyp  3
  THEN  Auto)

---

Home Index