---

{ [M:Type  Type]
    [P:lvProcess(lp.M[lp])]. [ms:process-Input(lp.M[lp])].
      (P(ms)  lvProcess(lp.M[lp])  process-Output(lp.M[lp])) 
    supposing A,B:Type.  ((A r B)  (M[A] r M[B])) }

{ Proof }

---

Definitions occuring in Statement :  process-apply: P(ms),  process-Output: process-Output(lp.M[lp]),  process-Input: process-Input(lp.M[lp]),  lvProcess: lvProcess(lp.M[lp]),  subtype_rel: A r B,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  all: x:A. B[x],  implies: P  Q,  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  universe: Type
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  implies: P  Q,  so_apply: x[s],  member: t  T,  process-apply: P(ms),  so_lambda: x.t[x]
Lemmas :  process-Output_wf,  process-Input_wf,  lvProcess_wf,  Process-subtype

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[P:lvProcess(lp.M[lp])].  \mforall{}[ms:process-Input(lp.M[lp])].
        (P(ms)  \mmember{}  lvProcess(lp.M[lp])  \mtimes{}  process-Output(lp.M[lp])) 
    supposing  \mforall{}A,B:Type.    ((A  \msubseteq{}r  B)  {}\mRightarrow{}  (M[A]  \msubseteq{}r  M[B]))


Date html generated: 2011_08_17-PM-06_38_28
Last ObjectModification: 2011_06_18-PM-12_04_04

Home Index