---

{ [M:Type  Type]
    [n,m:].
      process-input'(lp.M[lp];m) r process-input'(lp.M[lp];n) supposing m  n 
    supposing A,B:Type.  ((A r B)  (M[A] r M[B])) }

{ Proof }

---

Definitions occuring in Statement :  process-input': process-input'(lp.M[lp];n),  subtype_rel: A r B,  nat: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  le: A  B,  all: x:A. B[x],  implies: P  Q,  function: 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],  process-input': process-input'(lp.M[lp];n),  member: t  T,  int_seg: {i..j},  so_lambda: x.t[x],  lelt: i  j < k,  and: P  Q,  nat: ,  prop:
Lemmas :  subtype_rel_product,  int_seg_wf,  le_wf,  nat_properties,  subtype_rel_self,  nat_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[n,m:\mBbbN{}].    process-input'(lp.M[lp];m)  \msubseteq{}r  process-input'(lp.M[lp];n)  supposing  m  \mleq{}  n 
    supposing  \mforall{}A,B:Type.    ((A  \msubseteq{}r  B)  {}\mRightarrow{}  (M[A]  \msubseteq{}r  M[B]))


Date html generated: 2011_08_17-PM-06_36_52
Last ObjectModification: 2011_06_18-PM-12_00_22

Home Index