---

{ [M:Type  Type]
    [m:]. [P:lvprocess(lp.M[lp];m)]. [ms:input(lp.M[lp];m)].
      (P(ms)  lvprocess(lp.M[lp];m)
                ((Id  process-input'(lp.M[lp];m)) List)) 
    supposing A,B:Type.  ((A r B)  (M[A] r M[B])) }

{ Proof }

---

Definitions occuring in Statement :  process-apply: P(ms),  process-input': process-input'(lp.M[lp];n),  process-input: input(lp.M[lp];n),  lvprocess: lvprocess(lp.M[lp];n),  Id: Id,  subtype_rel: A r B,  nat: ,  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],  list: type List,  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],  ext-eq: A  B,  and: P  Q
Lemmas :  Id_wf,  process-input'_wf,  process-input_wf,  lvprocess_wf,  nat_wf,  process-ext-eq

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[m:\mBbbN{}].  \mforall{}[P:lvprocess(lp.M[lp];m)].  \mforall{}[ms:input(lp.M[lp];m)].
        (P(ms)  \mmember{}  lvprocess(lp.M[lp];m)  \mtimes{}  ((Id  \mtimes{}  process-input'(lp.M[lp];m))  List)) 
    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_37
Last ObjectModification: 2011_06_18-PM-12_04_19

Home Index