---

{ n2m:  Message. l2m:Id  Message.
    [A1,A2:EnvType  RunType  '].
      S1,S2:InitSys.
        [B1,B2:EO'  '].
          ((env:EnvType. r:RunType.  (A2[env;r]  A1[env;r]))
           (eo:EO'. (B1[eo]  B2[eo]))
           S1  S2
           assuming(env,r.A1[env;r])
              S1 |= eo.B1[eo]
           assuming(env,r.A2[env;r])
              S2 |= eo.B2[eo]) }

{ Proof }

---

Definitions occuring in Statement :  strong-realizes: strong-realizes,  subsys: S1  S2,  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],  all: x:A. B[x],  implies: P  Q,  function: x:A  B[x]
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  prop: ,  implies: P  Q,  so_apply: x[s1;s2],  so_apply: x[s],  strong-realizes: strong-realizes,  system-strongly-realizes: system-strongly-realizes,  InitialSystem: InitialSystem(P.M[P]),  member: t  T,  so_lambda: x y.t[x; y],  so_lambda: x.t[x],  EnvType: EnvType,  RunType: RunType,  system-realizes: system-realizes,  pEnvType: pEnvType(T.M[T]),  let: let,  Message: Message,  InitSys: InitSys,  System: System(P.M[P]),  Sys: Sys,  uimplies: b supposing a,  subsys: S1  S2,  runEO: runEO(n2m;l2m;env;S),  stdEO: stdEO(n2m;l2m;env;S),  guard: {T}
Lemmas :  strong-realizes_wf,  RunType_wf,  EnvType_wf,  event-ordering+_wf,  Message_wf,  subsys_wf,  InitSys_wf,  Id_wf,  nat_wf,  subsys_transitivity,  pRun_wf,  name_wf,  mData_wf,  strong-continuous-product,  continuous-constant,  fulpRunType-subtype,  stdEO_wf

---

\mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  Message.  \mforall{}l2m:Id  {}\mrightarrow{}  Message.
    \mforall{}[A1,A2:EnvType  {}\mrightarrow{}  RunType  {}\mrightarrow{}  \mBbbP{}'].
        \mforall{}S1,S2:InitSys.
            \mforall{}[B1,B2:EO'  {}\mrightarrow{}  \mBbbP{}'].
                ((\mforall{}env:EnvType.  \mforall{}r:RunType.    (A2[env;r]  {}\mRightarrow{}  A1[env;r]))
                {}\mRightarrow{}  (\mforall{}eo:EO'.  (B1[eo]  {}\mRightarrow{}  B2[eo]))
                {}\mRightarrow{}  S1  \msubseteq{}  S2
                {}\mRightarrow{}  assuming(env,r.A1[env;r])
                        S1  |=  eo.B1[eo]
                {}\mRightarrow{}  assuming(env,r.A2[env;r])
                        S2  |=  eo.B2[eo])


Date html generated: 2011_08_17-PM-04_13_45
Last ObjectModification: 2011_06_18-AM-11_32_02

Home Index