---

Step * of Lemma Kleene-M_wf

∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ].  (Kleene-M(F) ∈ ⇃(basic-strong-continuity(T;F)))
BY
{ ((Auto
    THEN (Assert λn,f. ν(v.F (λx.if (x) < (0)  then ⊥  else if (x) < (n)  then f x  else (exception(v; x)))?v:x.<x, x>) \000C∈ ⇃({M:n:ℕ ⟶ (ℕn ⟶ T) ⟶ (ℕ ⋃ (ℕ × ℕ))| 
                                    ∀f:ℕ ⟶ T
                                      ((∃n:ℕ. ((M n f) = (F f) ∈ ℕ))
                                      ∧ (∀n:ℕ. (M n f) = (F f) ∈ ℕ supposing M n f is an integer)
                                      ∧ (∀n,m:ℕ.  ((n ≤ m) ⇒ M n f is an integer ⇒ M m f is an integer)))} ) BY
                (Refine_StrongContinuity2 THEN Auto))
    )
   THEN Fold `bound-domain` (-1)
   THEN Fold `Kleene-M` (-1)
   THEN Fold `sq_exists` (-1)
   THEN Fold `basic-strong-continuity` (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:\{T:Type|  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)\}  ].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].
    (Kleene-M(F)  \mmember{}  \00D9(basic-strong-continuity(T;F)))


By

---

Latex:
((Auto
    THEN  (Assert  \mlambda{}n,f.  \mnu{}(v.F 
                                                  (\mlambda{}x.if  (x)  <  (0)
                                                                then  \mbot{}
                                                                else  if  (x)  <  (n)    then  f  x    else  (exception(v;  x)))?v:x.<x,  x>)  \mmember{}  \00D9\000C(\{M:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  T)  {}\mrightarrow{}  (\mBbbN{}  \mcup{}  (\mBbbN{}  \mtimes{}  \mBbbN{}))| 
                                                                    \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T
                                                                        ((\mexists{}n:\mBbbN{}.  ((M  n  f)  =  (F  f)))
                                                                        \mwedge{}  (\mforall{}n:\mBbbN{}.  (M  n  f)  =  (F  f)  supposing  M  n  f  is  an  integer)
                                                                        \mwedge{}  (\mforall{}n,m:\mBbbN{}.
                                                                                  ((n  \mleq{}  m)
                                                                                  {}\mRightarrow{}  M  n  f  is  an  integer
                                                                                  {}\mRightarrow{}  M  m  f  is  an  integer)))\}  )  BY
                            (Refine\_StrongContinuity2  THEN  Auto))
    )
  THEN  Fold  `bound-domain`  (-1)
  THEN  Fold  `Kleene-M`  (-1)
  THEN  Fold  `sq\_exists`  (-1)
  THEN  Fold  `basic-strong-continuity`  (-1)
  THEN  Auto)

---

Home Index