---

Step * of Lemma strong-continuity2-half-squash-ext

∀[T:Type]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(strong-continuity2(T;F)) supposing (T ⊆r ℕ) ∧ (↓T)
BY
{ Extract of Obid: strong-continuity2-half-squash
  not unfolding  Kleene-M KleeneM KleeneSearch mu int? is_int
  finishing with Auto
  normalizes to:
  
  λF.<λn,f. eval v = Kleene-M(F) n f in if v is an integer then inl v else inr Ax 
     , λf.<<mu(λn.is_int(Kleene-M(F) n f)), Ax>, λn.eval v = Kleene-M(F) n f in if v is an integer then Ax else Ax>
     > }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \00D9(strong-continuity2(T;F))  supposing  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)


By

---

Latex:
Extract  of  Obid:  strong-continuity2-half-squash
not  unfolding    Kleene-M  KleeneM  KleeneSearch  mu  int?  is\_int
finishing  with  Auto
normalizes  to:

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

---

Home Index