---

Step * 1 1 1 of Lemma compact-dCCC


1. K : Type
2. k : K
3. compact-type(K)
4. R : ℕ ⟶ K ⟶ 𝔹
5. d : ∀n:ℕ. ((∃m:K. (¬↑(R n m))) ∨ (∀m:K. (↑(R n m))))
6. n : ℕ
7. x : ∃m:K. (¬↑(R n m))
8. (d n) = (inl x) ∈ ((∃m:K. (¬↑(R n m))) ∨ (∀m:K. (↑(R n m))))
⊢ (↑(R n (fst(x)))) ⇒ (∀m:K. (↑(R n m)))
BY
{ (D -2 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  K  :  Type
2.  k  :  K
3.  compact-type(K)
4.  R  :  \mBbbN{}  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbB{}
5.  d  :  \mforall{}n:\mBbbN{}.  ((\mexists{}m:K.  (\mneg{}\muparrow{}(R  n  m)))  \mvee{}  (\mforall{}m:K.  (\muparrow{}(R  n  m))))
6.  n  :  \mBbbN{}
7.  x  :  \mexists{}m:K.  (\mneg{}\muparrow{}(R  n  m))
8.  (d  n)  =  (inl  x)
\mvdash{}  (\muparrow{}(R  n  (fst(x))))  {}\mRightarrow{}  (\mforall{}m:K.  (\muparrow{}(R  n  m)))


By

---

Latex:
(D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index