---

{ [S:InitSys]. [n2m:  Message]. [l2m:Id  Message]. [A:EnvType
                                                                RunType
                                                                '].
  [B:EO'  '].
    (assuming(env,r.A[env;r])
      S |= eo.B[eo]  ') }

{ Proof }

---

Definitions occuring in Statement :  strong-realizes: strong-realizes,  InitSys: InitSys,  RunType: RunType,  EnvType: EnvType,  Message: Message,  event-ordering+: EO+(Info),  Id: Id,  nat: ,  uall: [x:A]. B[x],  prop: ,  so_apply: x[s1;s2],  so_apply: x[s],  member: t  T,  function: x:A  B[x]
Definitions :  uall: [x:A]. B[x],  prop: ,  member: t  T,  InitSys: InitSys,  strong-realizes: strong-realizes,  so_apply: x[s1;s2],  so_apply: x[s],  InitialSystem: InitialSystem(P.M[P]),  so_lambda: x.t[x],  System: System(P.M[P]),  Sys: Sys,  so_lambda: x y.t[x; y],  uimplies: b supposing a,  Message: Message,  EnvType: EnvType,  RunType: RunType
Lemmas :  event-ordering+_wf,  Message_wf,  EnvType_wf,  RunType_wf,  Id_wf,  nat_wf,  InitSys_wf,  system-strongly-realizes_wf,  name_wf,  mData_wf,  strong-continuous-product,  continuous-constant

---

\mforall{}[S:InitSys].  \mforall{}[n2m:\mBbbN{}  {}\mrightarrow{}  Message].  \mforall{}[l2m:Id  {}\mrightarrow{}  Message].  \mforall{}[A:EnvType  {}\mrightarrow{}  RunType  {}\mrightarrow{}  \mBbbP{}'].
\mforall{}[B:EO'  {}\mrightarrow{}  \mBbbP{}'].
    (assuming(env,r.A[env;r])
        S  |=  eo.B[eo]  \mmember{}  \mBbbP{}')


Date html generated: 2011_08_17-PM-04_13_35
Last ObjectModification: 2011_06_18-AM-11_31_50

Home Index