---

Step * of Lemma strong-continuity2-implies-uniform-continuity-nat-ext

∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℕ)))
BY
{ Extract of Obid: strong-continuity2-implies-uniform-continuity-nat
  not unfolding  ucont Kleene-M primrec eq_int btrue bfalse 
  finishing with (RepUR ``let`` 0 THEN Auto)
  normalizes to:
  
  λF.ucont(F;λn,f. let M = λi.(Kleene-M(λf.(F (λx.if (f x =z 0) then ff else tt fi ))) i 
                               (λx.if f x then 1 else 0 fi )) in
                       case primrec(n;eval v = M n in
                                      if v is an integer then inl v
                                      else ff;λi,r. eval v = M i in if v is an integer then inr Ax  else r)
                        of inl(m) =>
                        inl m
                        | inr(x) =>
                        inr x ) }

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))


By

---

Latex:
Extract  of  Obid:  strong-continuity2-implies-uniform-continuity-nat
not  unfolding    ucont  Kleene-M  primrec  eq\_int  btrue  bfalse 
finishing  with  (RepUR  ``let``  0  THEN  Auto)
normalizes  to:

\mlambda{}F.ucont(F;\mlambda{}n,f.  let  M  =  \mlambda{}i.(Kleene-M(\mlambda{}f.(F  (\mlambda{}x.if  (f  x  =\msubz{}  0)  then  ff  else  tt  fi  )))  i 
                                                          (\mlambda{}x.if  f  x  then  1  else  0  fi  ))  in
                                          case  primrec(n;eval  v  =  M  n  in
                                                                        if  v  is  an  integer  then  inl  v
                                                                        else  ff;\mlambda{}i,r.  eval  v  =  M  i  in
                                                                                                if  v  is  an  integer  then  inr  Ax 
                                                                                                else  r)
                                            of  inl(m)  =>
                                            inl  m
                                            |  inr(x)  =>
                                            inr  x  )

---

Home Index