---

Step * of Lemma boot-process_wf

∀[M,E:Type ─→ Type].
  (∀[n:∩T:Type. E[T]]. ∀[f:∩T:Type. (M[T] ─→ (T?))].  (boot-process(f;n) ∈ process(P.M[P];P.E[P]))) supposing 
     (Continuous+(T.E[T]) and 
     Continuous+(T.M[T]))
BY
{ (ProveWfLemma THEN Using [`S',⌈λ2T.T?⌉] MemCD⋅ THEN Auto) }

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].
    (\mforall{}[n:\mcap{}T:Type.  E[T]].  \mforall{}[f:\mcap{}T:Type.  (M[T]  {}\mrightarrow{}  (T?))].
          (boot-process(f;n)  \mmember{}  process(P.M[P];P.E[P])))  supposing 
          (Continuous+(T.E[T])  and 
          Continuous+(T.M[T]))


By

(ProveWfLemma  THEN  Using  [`S',\mkleeneopen{}\mlambda{}\msubtwo{}T.T?\mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto)

---

Home Index