---

Step * of Lemma process-has-value

∀[M,E:Type ─→ Type].  ∀[P:process(P.M[P];P.E[P])]. (P)↓ supposing M[Top]
BY
{ (InstLemma `process-valueall-type` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (UnivCD THENA Auto)
   THEN BLemma `value-type-has-value`
   THEN EAuto 1) }

---

Latex:


\mforall{}[M,E:Type  {}\mrightarrow{}  Type].    \mforall{}[P:process(P.M[P];P.E[P])].  (P)\mdownarrow{}  supposing  M[Top]


By

(InstLemma  `process-valueall-type`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (UnivCD  THENA  Auto)
  THEN  BLemma  `value-type-has-value`
  THEN  EAuto  1)

---

Home Index