PropertyR ==
es:EO+(Info). e:E(Rcv). 
e':E(Send). ((e' < e) 
(Rcv(e) = Send(e')))
Definitions :
event-ordering+: EO+(Info),
ses-info: Info,
all: x:A. B[x],
exists: x:A. B[x],
es-E-interface: E(X),
and: P Q,
es-causl: (e < e'),
equal: s = t,
sdata: SecurityData,
ses-rcv: Rcv,
eclass-val: X(e),
ses-send: Send
FDL editor aliases :
ses-R
PropertyR == \mforall{}es:EO+(Info). \mforall{}e:E(Rcv). \mexists{}e':E(Send). ((e' < e) \mwedge{} (Rcv(e) = Send(e')))
Date html generated:
2010_08_28-AM-02_33_54
Last ObjectModification:
2010_02_22-PM-05_28_48
Home
Index