---

Step * of Lemma null-process_wf

∀[M,E:Type ⟶ Type].
  (∀[n:⋂T:Type. E[T]]. (null-process(n) ∈ process(P.M[P];P.E[P]))) supposing 
     (Continuous+(T.E[T]) and 
     Continuous+(T.M[T]))
BY
{ (ProveWfLemma
   THEN Using [`S',⌜λx.Unit⌝] MemCD⋅
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN Try ((ProveContinuous THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(ProveWfLemma
  THEN  Using  [`S',\mkleeneopen{}\mlambda{}x.Unit\mkleeneclose{}]  MemCD\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  Try  ((ProveContinuous  THEN  Auto)))

---

Home Index