---

Step * of Lemma weak-continuity-skolem-truncated

∀[T:{T:Type| (T ⊆r ℕ) ∧ (↓T)} ]. ∀F:(ℕ ⟶ T) ⟶ ℕ. ⇃(weak-continuity-skolem(T;F))
BY
{ (Auto
   THEN (Assert ⇃(basic-strong-continuity(T;F)) BY
               (UseWitness ⌜Kleene-M(F)⌝⋅ THEN Auto))
   THEN ParallelLast
   THEN EAuto 2) }

---

Latex:

---

Latex:
\mforall{}[T:\{T:Type|  (T  \msubseteq{}r  \mBbbN{})  \mwedge{}  (\mdownarrow{}T)\}  ].  \mforall{}F:(\mBbbN{}  {}\mrightarrow{}  T)  {}\mrightarrow{}  \mBbbN{}.  \00D9(weak-continuity-skolem(T;F))


By

---

Latex:
(Auto
  THEN  (Assert  \00D9(basic-strong-continuity(T;F))  BY
                          (UseWitness  \mkleeneopen{}Kleene-M(F)\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  ParallelLast
  THEN  EAuto  2)

---

Home Index