Nuprl Definition : send-rcv-match
send-rcv-match(m1;m2) == (↑m1 ∈b Send) ∧ (↑m2 ∈b Rcv) ∧ (m1 < m2) ∧ (Send(m1) = Rcv(m2) ∈ SecurityData)
Definitions occuring in Statement :
ses-rcv: Rcv,
ses-send: Send,
sdata: SecurityData,
eclass-val: X(e),
in-eclass: e ∈b X,
es-causl: (e < e'),
assert: ↑b,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
send-rcv-match
Latex:
send-rcv-match(m1;m2) == (\muparrow{}m1 \mmember{}\msubb{} Send) \mwedge{} (\muparrow{}m2 \mmember{}\msubb{} Rcv) \mwedge{} (m1 < m2) \mwedge{} (Send(m1) = Rcv(m2))
Date html generated:
2015_07_23-PM-00_09_28
Last ObjectModification:
2012_08_30-PM-04_27_18
Home
Index