---

{ [M:Type  Type]. [n:].  (null-process()  lvprocess(lp.M[lp];n)) }

{ Proof }

---

Definitions occuring in Statement :  lvprocess: lvprocess(lp.M[lp];n),  nat: ,  uall: [x:A]. B[x],  so_apply: x[s],  member: t  T,  function: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  member: t  T,  so_apply: x[s],  null-process: null-process(),  so_lambda: x.t[x]
Lemmas :  stateless-process_wf,  Id_wf,  process-input'_wf,  process-input_wf,  nat_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[n:\mBbbN{}].    (null-process()  \mmember{}  lvprocess(lp.M[lp];n))


Date html generated: 2011_08_17-PM-06_37_59
Last ObjectModification: 2011_06_18-PM-12_02_06

Home Index