Nuprl Definition : ses-R
PropertyR == ∀es:EO+(Info). ∀e:E(Rcv). ∃e':E(Send). ((e' < e) ∧ (Rcv(e) = Send(e') ∈ SecurityData))
Definitions occuring in Statement :
ses-rcv: Rcv,
ses-send: Send,
ses-info: Info,
sdata: SecurityData,
es-E-interface: E(X),
eclass-val: X(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
ses-R
Latex:
PropertyR == \mforall{}es:EO+(Info). \mforall{}e:E(Rcv). \mexists{}e':E(Send). ((e' < e) \mwedge{} (Rcv(e) = Send(e')))
Date html generated:
2015_07_23-PM-00_07_24
Last ObjectModification:
2012_08_30-PM-04_24_21
Home
Index