---

{ Cs:Component List
    assuming(env,r.reliable-env(env; r))
     mk-init-sys(Cs) |= es.cause:E  (E?)
                            (CCs.e:E
                                     pProc-out-at(es;snd(C);e).
                                      let y,c = p 
                                      in e':E
                                          ((loc(e') = y)
                                           (e < e')
                                           (info(e') = comm-msg(c))
                                           ((cause e') = (inl e ))) 
                                         supposing com-kind(c) = "msg" 
                                     supposing loc(e) = (fst(C))) }

{ Proof }

---

Definitions occuring in Statement :  std-l2m: std-l2m(),  std-n2m: std-n2m(),  strong-realizes: strong-realizes,  mk-init-sys: mk-init-sys(Cs),  Component: Component,  Proc-out-at: Proc-out-at(es;P;e),  Message: Message,  reliable-env: reliable-env(env; r),  comm-msg: comm-msg(c),  com-kind: com-kind(c),  lg-all: xG.P[x],  es-info: info(e),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  uimplies: b supposing a,  pi1: fst(t),  pi2: snd(t),  all: x:A. B[x],  exists: x:A. B[x],  and: P  Q,  unit: Unit,  apply: f a,  function: x:A  B[x],  spread: spread def,  inl: inl x ,  union: left + right,  list: type List,  token: "$token",  atom: Atom,  equal: s = t,  l_all: (xL.P[x])
Definitions :  all: x:A. B[x],  exists: x:A. B[x],  uimplies: b supposing a,  pi1: fst(t),  pi2: snd(t),  and: P  Q,  Message: Message,  implies: P  Q,  member: t  T,  so_lambda: x.t[x],  prop: ,  InitSys: InitSys,  pMsg: pMsg(P.M[P]),  so_lambda: x y.t[x; y],  l_all: (xL.P[x]),  ProcOut: ProcOut,  Proc: Proc,  pExt: pExt(P.M[P]),  or: P  Q,  cand: A c B,  Component: Component,  let: let,  uall: [x:A]. B[x],  so_apply: x[s],  component: component(P.M[P]),  Sys: Sys,  so_apply: x[s1;s2],  guard: {T},  sq_type: SQType(T),  iff: P  Q,  rev_implies: P  Q,  command-to-msg: command-to-msg(c;nmsg;lmsg),  not: A,  false: False,  ifthenelse: if b then t else f fi ,  btrue: tt,  bfalse: ff,  subtype: S  T,  ProcOut-all: ProcOut-all(G;p.P[p]),  mk-init-sys: mk-init-sys(Cs),  Proc-out-at: Proc-out-at(es;P;e)
Lemmas :  components-realize,  std-n2m_wf,  std-l2m_wf,  pCom_wf,  name_wf,  mData_wf,  Component_wf,  reliable-env_wf2,  RunType_wf,  EnvType_wf,  mk-init-sys_wf,  event-ordering+_inc,  es-E_wf,  unit_wf,  l_all_wf2,  ProcOut-all_wf,  com-kind_wf,  l_member_wf,  es-loc_wf,  es-causl_wf,  nat_wf,  es-info_wf,  command-to-msg_wf,  Id_wf,  comm-msg_wf,  Sys_wf,  std-initial_wf,  strong-realizes_functionality,  subsys_weakening,  lg-all_functionality,  Proc-out-at_wf,  subtype_rel_self,  ldag_wf,  Message_wf,  subtype_base_sq,  atom_subtype_base,  cons_member,  eq_atom_wf,  bool_wf,  assert_wf,  not_wf,  bnot_wf,  bool_cases,  bool_subtype_base,  iff_weakening_uiff,  uiff_transitivity,  eqtt_to_assert,  assert_of_eq_atom,  eqff_to_assert,  assert_of_bnot,  not_functionality_wrt_uiff

---

\mforall{}Cs:Component  List
    assuming(env,r.reliable-env(env;  r))
      mk-init-sys(Cs)  |=  es.\mexists{}cause:E  {}\mrightarrow{}  (E?)
                                                    (\mforall{}C\mmember{}Cs.\mforall{}e:E
                                                                      \mforall{}p\mmember{}Proc-out-at(es;snd(C);e).let  y,c  =  p 
                                                                                                                              in  \mexists{}e':E
                                                                                                                                      ((loc(e')  =  y)
                                                                                                                                      \mwedge{}  (e  <  e')
                                                                                                                                      \mwedge{}  (info(e')  =  comm-msg(c))
                                                                                                                                      \mwedge{}  ((cause  e')  =  (inl  e  ))) 
                                                                                                                                    supposing  com-kind(c)  =  "msg" 
                                                                      supposing  loc(e)  =  (fst(C)))


Date html generated: 2011_08_17-PM-04_14_21
Last ObjectModification: 2011_06_18-AM-11_32_38

Home Index