---

{ [M:Type  Type]
    S0:InitialSystem(P.M[P]). n2m:  pMsg(P.M[P]). l2m:Id  pMsg(P.M[P]).
    env:pEnvType(P.M[P]). e1,e2:E.
      (e1 loc e2 
       (run-event-loc(e1) = run-event-loc(e2))
           (run-event-step(e1)  run-event-step(e2))) 
    supposing Continuous+(P.M[P]) }

{ Proof }

---

Definitions occuring in Statement :  stdEO: stdEO(n2m;l2m;env;S),  InitialSystem: InitialSystem(P.M[P]),  run-event-step: run-event-step(e),  run-event-loc: run-event-loc(e),  pEnvType: pEnvType(T.M[T]),  pMsg: pMsg(P.M[P]),  es-le: e loc e' ,  es-E: E,  Id: Id,  strong-type-continuous: Continuous+(T.F[T]),  nat: ,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  le: A  B,  all: x:A. B[x],  iff: P  Q,  and: P  Q,  function: x:A  B[x],  universe: Type,  equal: s = t
Definitions :  uall: [x:A]. B[x],  uimplies: b supposing a,  strong-type-continuous: Continuous+(T.F[T]),  so_apply: x[s],  all: x:A. B[x],  iff: P  Q,  and: P  Q,  le: A  B,  member: t  T,  ext-eq: A  B,  implies: P  Q,  rev_implies: P  Q,  pRunType: pRunType(T.M[T]),  fulpRunType: fulpRunType(T.M[T]),  so_lambda: x.t[x],  top: Top,  not: A,  false: False,  prop: ,  stdEO: stdEO(n2m;l2m;env;S),  es-loc: loc(e),  runEO: runEO(n2m;l2m;env;S),  run-eo: EO(r),  mk-eo: mk-eo(E;dom;l;R;a;b;c;d;e;f),  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  bfalse: ff,  btrue: tt,  es-le: e loc e' ,  or: P  Q,  guard: {T},  InitialSystem: InitialSystem(P.M[P]),  nat: ,  es-E: E,  System: System(P.M[P]),  es-locl: (e <loc e'),  subtype: S  T
Lemmas :  stdEO-causal,  nat_wf,  pRun_wf,  subtype_rel_function,  Id_wf,  pMsg_wf,  unit_wf,  System_wf,  top_wf,  ldag_wf,  pInTransit_wf,  subtype_rel_self,  subtype_rel_simple_product,  fulpRunType_wf,  pRunType_wf,  run-event-step_wf,  es-le_wf,  stdEO_wf,  event-ordering+_inc,  event-ordering+_wf,  run-event-loc_wf,  le_wf,  es-E_wf,  pEnvType_wf,  InitialSystem_wf,  strong-type-continuous_wf,  es-le-loc,  es-locl-total,  es-le_weakening,  es-locl_wf

---

\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}S0:InitialSystem(P.M[P]).  \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
    \mforall{}e1,e2:E.
        (e1  \mleq{}loc  e2 
        \mLeftarrow{}{}\mRightarrow{}  (run-event-loc(e1)  =  run-event-loc(e2))  \mwedge{}  (run-event-step(e1)  \mleq{}  run-event-step(e2))) 
    supposing  Continuous+(P.M[P])


Date html generated: 2011_08_17-PM-03_41_35
Last ObjectModification: 2011_06_18-AM-11_23_02

Home Index