---

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

∀F:(ℕ ⟶ 𝔹) ⟶ 𝔹. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ F f = F g))
BY
{ Extract of Obid: strong-continuity2-implies-uniform-continuity
  not unfolding  bottom primrec ucont eq_int btrue bfalse Kleene-M mu
  finishing with (RepUR ``let`` 0 THEN Auto)
  normalizes to:
  
  λF.ucont(F;λn,f. let M = λi.(Kleene-M(λf.if F (λx.if (f x =z 0) then ff else tt fi ) then 1 else 0 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 if (m) < (2)  then if m=0 then ff else if m=1 then tt else (fst(Ax))  else ff
                        | inr(x) =>
                        inr x ) }

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbB{}.  \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
not  unfolding    bottom  primrec  ucont  eq\_int  btrue  bfalse  Kleene-M  mu
finishing  with  (RepUR  ``let``  0  THEN  Auto)
normalizes  to:

\mlambda{}F.ucont(F;\mlambda{}n,f.  let  M  =  \mlambda{}i.(Kleene-M(\mlambda{}f.if  F  (\mlambda{}x.if  (f  x  =\msubz{}  0)  then  ff  else  tt  fi  )
                                                                                  then  1
                                                                                  else  0
                                                                                  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  if  (m)  <  (2)
                                                          then  if  m=0  then  ff  else  if  m=1  then  tt  else  (fst(Ax))
                                                          else  ff
                                            |  inr(x)  =>
                                            inr  x  )

---

Home Index