Nuprl Definition : info-delivered
info-delivered{i:l}(Info;X) ==
∀es:EO+(Info). ∀e:E. ∀locnfo:Id × Info.
(locnfo ∈ X(e) ⇒ (∃e':E. ((e < e') ∧ (loc(e') = (fst(locnfo)) ∈ Id) ∧ (info(e') = (snd(locnfo)) ∈ Info))))
Definitions occuring in Statement :
classrel: v ∈ X(e),
es-info: info(e),
event-ordering+: EO+(Info),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
pi1: fst(t),
pi2: snd(t),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
info-delivered
Latex:
info-delivered\{i:l\}(Info;X) ==
\mforall{}es:EO+(Info). \mforall{}e:E. \mforall{}locnfo:Id \mtimes{} Info.
(locnfo \mmember{} X(e) {}\mRightarrow{} (\mexists{}e':E. ((e < e') \mwedge{} (loc(e') = (fst(locnfo))) \mwedge{} (info(e') = (snd(locnfo))))))
Date html generated:
2015_07_21-PM-04_51_03
Last ObjectModification:
2013_02_14-PM-10_25_51
Home
Index