---

Step * of Lemma decidable-finite-cantor-ext

∀[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
{ Extract of Obid: decidable-finite-cantor
  not unfolding  primrec listops boolops btrue bfalse
  finishing with xxxTry ((Fold `finite-cantor-decider` 0 THEN Auto))xxx
  normalizes to:
  
  λdcdr,n,F. finite-cantor-decider(dcdr;n;F) }

---

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:
Extract  of  Obid:  decidable-finite-cantor
not  unfolding    primrec  listops  boolops  btrue  bfalse
finishing  with  xxxTry  ((Fold  `finite-cantor-decider`  0  THEN  Auto))xxx
normalizes  to:

\mlambda{}dcdr,n,F.  finite-cantor-decider(dcdr;n;F)

---

Home Index