---

Step * of Lemma KleeneM_wf

∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀[F:(ℕ ⟶ T) ⟶ ℕ]. ∀[f:ℕ ⟶ T].
  (KleeneM(F;f) ∈ ⇃({m:ℕ+| ∀g:ℕ ⟶ T. ((g = f ∈ (ℕm ⟶ T)) ⇒ ((F g) = (F f) ∈ ℤ))} ))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:\{T:Type|  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)\}  ].  \mforall{}[F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[f:\mBbbN{}  {}\mrightarrow{}  T].
    (KleeneM(F;f)  \mmember{}  \00D9(\{m:\mBbbN{}\msupplus{}|  \mforall{}g:\mBbbN{}  {}\mrightarrow{}  T.  ((g  =  f)  {}\mRightarrow{}  ((F  g)  =  (F  f)))\}  ))


By

---

Latex:
ProveWfLemma

---

Home Index