---

hdr.X <-- p.Z[p] ==
  e':E. v:T.
    (v  X(e')
     (e,start:E
          p:A
           (start loc e   (e < e')  <loc(e'), make-Msg(hdr;T;v)>  Z[p](e))))

---

Definitions occuring in Statement :  Message: Message,  classrel: v  X(e),  eo-forward: eo.e,  es-le: e loc e' ,  es-causl: (e < e'),  es-loc: loc(e),  es-E: E,  Id: Id,  all: x:A. B[x],  exists: x:A. B[x],  squash: T,  implies: P  Q,  and: P  Q,  pair: <a, b>,  product: x:A  B[x]
FDL editor aliases :  base-class-caused-by

---

hdr.X  <--  p.Z[p]  ==
    \mforall{}e':E.  \mforall{}v:T.
        (v  \mmember{}  X(e')
        {}\mRightarrow{}  (\mdownarrow{}\mexists{}e,start:E.  \mexists{}p:A.  (start  \mleq{}loc  e    \mwedge{}  (e  <  e')  \mwedge{}  <loc(e'),  make-Msg(hdr;T;v)>  \mmember{}  Z[p](e))))


Date html generated: 2011_08_17-PM-04_05_49
Last ObjectModification: 2011_07_22-PM-12_08_26

Home Index