---

{ n2m:  Message. l2m:Id  Message. Cs:Component List.
    assuming(env,r.reliable-env(env; r))
     <Cs, lg-nil()> |=
     es.cause:E  (E?)
         (CCs.e:E
                  let G = last(data-stream(snd(C);map(e.info(e);loc(e)))) in
                      pG.let y,c = p 
                           in (com-kind(c)  ``msg choose new``)
                               (e':E
                                   ((loc(e') = y)
                                    (e < e')
                                    (n:
                                       nm:Id
                                        (info(e')
                                        = command-to-msg(c;n2m n;l2m nm)))
                                    ((cause e') = (inl e )))) 
                  supposing loc(e) = (fst(C))) }

{ Proof }

---

Definitions occuring in Statement :  strong-realizes: strong-realizes,  Component: Component,  Message: Message,  command-to-msg: command-to-msg(c;nmsg;lmsg),  reliable-env: reliable-env(env; r),  com-kind: com-kind(c),  lg-all: xG.P[x],  lg-nil: lg-nil(),  es-info: info(e),  es-le-before: loc(e),  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  data-stream: data-stream(P;L),  Id: Id,  map: map(f;as),  nat: ,  let: let,  uimplies: b supposing a,  pi1: fst(t),  pi2: snd(t),  all: x:A. B[x],  exists: x:A. B[x],  implies: P  Q,  and: P  Q,  unit: Unit,  apply: f a,  lambda: x.A[x],  function: x:A  B[x],  spread: spread def,  pair: <a, b>,  inl: inl x ,  union: left + right,  cons: [car / cdr],  nil: [],  list: type List,  token: "$token",  atom: Atom,  equal: s = t,  l_all: (xL.P[x]),  last: last(L),  l_member: (x  l)
Definitions :  Message: Message,  Component: Component,  strong-realizes: strong-realizes,  pMsg: pMsg(P.M[P]),  so_lambda: x.t[x],  member: t  T,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s]
Lemmas :  std-components-property,  name_wf,  mData_wf,  strong-continuous-product,  continuous-constant

---

\mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  Message.  \mforall{}l2m:Id  {}\mrightarrow{}  Message.  \mforall{}Cs:Component  List.
    assuming(env,r.reliable-env(env;  r))
      <Cs,  lg-nil()>  |=  es.\mexists{}cause:E  {}\mrightarrow{}  (E?)
                                                  (\mforall{}C\mmember{}Cs.\mforall{}e:E
                                                                    let  G  =  last(data-stream(snd(C);map(\mlambda{}e.info(e);\mleq{}loc(e))))  in
                                                                            \mforall{}p\mmember{}G.let  y,c  =  p 
                                                                                      in  (com-kind(c)  \mmember{}  ``msg  choose  new``)
                                                                                            {}\mRightarrow{}  (\mexists{}e':E
                                                                                                      ((loc(e')  =  y)
                                                                                                      \mwedge{}  (e  <  e')
                                                                                                      \mwedge{}  (\mexists{}n:\mBbbN{}
                                                                                                              \mexists{}nm:Id
                                                                                                                (info(e')  =  command-to-msg(c;n2m  n;l2m  nm)))
                                                                                                      \mwedge{}  ((cause  e')  =  (inl  e  )))) 
                                                                    supposing  loc(e)  =  (fst(C)))


Date html generated: 2011_08_17-PM-04_14_06
Last ObjectModification: 2011_06_18-AM-11_32_26

Home Index