---

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

∀F:(ℕ ⟶ 𝔹) ⟶ ℤ. ⇃(∃n:ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕn ⟶ 𝔹)) ⇒ ((F f) = (F g) ∈ ℤ)))
BY
{ Extract of Obid: strong-continuity2-implies-uniform-continuity-int
  not unfolding  ucont bottom bar_recursion mu_ge primrec Kleene-M int?
  finishing with (RepUR ``let int2nat nat2int`` 0 THEN Auto)
  normalizes to:
  
  λF.ucont(F;λn,f. let M = λi.(Kleene-M(λf.if (F (λx.if f x=0 then inr Ax  else (inl Ax))) < (0)
                                              then (2 * ((-(F (λx.if f x=0 then inr Ax  else (inl Ax)))) - 1)) + 1
                                              else (2 * (F (λx.if f x=0 then inr Ax  else (inl Ax))))) 
                               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 inr Ax ;λi,r. eval v = M i in if v is an integer then inr Ax  else r)
                        of inl(m) =>
                        inl let q,r = divrem(m; 2) 
                            in if r=0 then q else (-(q + 1))
                        | inr(x) =>
                        inr x ) }

---

Latex:

---

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbZ{}.  \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-int
not  unfolding    ucont  bottom  bar\_recursion  mu\_ge  primrec  Kleene-M  int?
finishing  with  (RepUR  ``let  int2nat  nat2int``  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=0  then  inr  Ax    else  (inl  Ax)))  <  (0)
                                                                                        then  (2
                                                                                                  *  ((-(F  (\mlambda{}x.if  f  x=0  then  inr  Ax    else  (inl  Ax)))) 
                                                                                                      -  1))
                                                                                                  +  1
                                                                                        else  (2
                                                                                                  *  (F  (\mlambda{}x.if  f  x=0  then  inr  Ax    else  (inl  Ax))))) 
                                                          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  inr  Ax  ;\mlambda{}i,r.  eval  v  =  M  i  in
                                                                                                          if  v  is  an  integer  then  inr  Ax 
                                                                                                          else  r)
                                            of  inl(m)  =>
                                            inl  let  q,r  =  divrem(m;  2) 
                                                    in  if  r=0  then  q  else  (-(q  +  1))
                                            |  inr(x)  =>
                                            inr  x  )

---

Home Index