---

Step * of Lemma simple-decidable-finite-cantor-ext

∀[T:Type]. ∀[R:T ⟶ ℙ].  ((∀x:T. Dec(R[x])) ⇒ (∀n:ℕ. ∀F:(ℕn ⟶ 𝔹) ⟶ T.  Dec(∃f:ℕn ⟶ 𝔹. R[F f])))
BY
{ Extract of Obid: simple-decidable-finite-cantor
  not unfolding  primrec listops boolops btrue bfalse
  finishing with xxx(Try (Fold `simple-finite-cantor-decider` 0) THEN Auto)xxx
  normalizes to:
  
  λdcdr,n,F. FiniteCantorDecide(dcdr;n;F) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  simple-decidable-finite-cantor
not  unfolding    primrec  listops  boolops  btrue  bfalse
finishing  with  xxx(Try  (Fold  `simple-finite-cantor-decider`  0)  THEN  Auto)xxx
normalizes  to:

\mlambda{}dcdr,n,F.  FiniteCantorDecide(dcdr;n;F)

---

Home Index