---

Step * of Lemma basic-implies-strong-continuity2-ext

∀[T:Type]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (basic-strong-continuity(T;F) ⇒ strong-continuity2(T;F))
BY
{ Extract of Obid: basic-implies-strong-continuity2
  not unfolding  isint mu primrec
  finishing with (RepUR ``int? is_int btrue bfalse it`` 0 THEN Auto)
  normalizes to:
  
  λM.<λn,f. eval v = M n f in if v is an integer then inl v else ff
     , λf.<<mu(λn.is_int(M n f)), Ax>, λn.eval v = M n f in if v is an integer then Ax else Ax>
     > }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].    (basic-strong-continuity(T;F)  {}\mRightarrow{}  strong-continuity2(T;F))


By

---

Latex:
Extract  of  Obid:  basic-implies-strong-continuity2
not  unfolding    isint  mu  primrec
finishing  with  (RepUR  ``int?  is\_int  btrue  bfalse  it``  0  THEN  Auto)
normalizes  to:

\mlambda{}M.<\mlambda{}n,f.  eval  v  =  M  n  f  in  if  v  is  an  integer  then  inl  v  else  ff
      ,  \mlambda{}f.<<mu(\mlambda{}n.is\_int(M  n  f)),  Ax>,  \mlambda{}n.eval  v  =  M  n  f  in  if  v  is  an  integer  then  Ax  else  Ax>
      >

---

Home Index