---

Step * 1 1 of Lemma d-CCC-finite


1. [T] : Type
2. finite(T)
3. ∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))
4. R : ℕ ⟶ T ⟶ 𝔹
5. d : ∀n:ℕ. Dec(∃m:T. (¬↑(R n m)))
6. t : T
7. n : ℕ
8. ↑(R n case d n of inl(a) => fst(a) | inr(_) => t)
⊢ ∀m:T. (↑(R n m))
BY
{ (MoveToConcl (-1) THEN (GenConclTerm ⌜d n⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN Reduce 0) }

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

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

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  finite(T)
3.  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}t:T.  Dec(P[t]))  {}\mRightarrow{}  Dec(\mexists{}t:T.  P[t]))
4.  R  :  \mBbbN{}  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
5.  d  :  \mforall{}n:\mBbbN{}.  Dec(\mexists{}m:T.  (\mneg{}\muparrow{}(R  n  m)))
6.  t  :  T
7.  n  :  \mBbbN{}
8.  \muparrow{}(R  n  case  d  n  of  inl(a)  =>  fst(a)  |  inr($_{}$)  =>  t)
\mvdash{}  \mforall{}m:T.  (\muparrow{}(R  n  m))


By

---

Latex:
(MoveToConcl  (-1)  THEN  (GenConclTerm  \mkleeneopen{}d  n\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1  THEN  Reduce  0)

---

Home Index