---

Step * of Lemma decidable-finite-cantor

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  Dec(R[x;y])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.  Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])))
BY
{ Auto }

1
.....decidable?..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. n : ℕ
5. F : (ℕn ⟶ 𝔹) ⟶ T
⊢ Dec(∃f,g:ℕn ⟶ 𝔹. R[F f;F g])

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:T.    Dec(R[x;y]))  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  \mforall{}F:(\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  T.    Dec(\mexists{}f,g:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.  R[F  f;F  g])))


By

---

Latex:
Auto

---

Home Index