Nuprl Definition : es-class-mcast-fail
∀e,x,y. e∈X(x) mcast to each of locs a
Y(y) such that
R[e; x; y]
unless loc(e) ∈ failset ==
(∀e:E(Y). ((loc(e) ∈ locs) ∧ (∃e':E(X). (e' c≤ e ∧ R[e'; X(e'); Y(e)]))))
∧ (∀e':E(X). ((∀i∈locs.∃e:E(Y). ((loc(e) = i ∈ Id) ∧ e' c≤ e ∧ R[e'; X(e'); Y(e)])) ∨ (loc(e') ∈ failset)))
Definitions occuring in Statement :
es-E-interface: E(X),
eclass-val: X(e),
es-causle: e c≤ e',
es-loc: loc(e),
Id: Id,
l_all: (∀x∈L.P[x]),
l_member: (x ∈ l),
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
or: P ∨ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
es-class-mcast-fail
Latex:
\mforall{}e,x,y. e\mmember{}X(x) mcast to each of locs a
Y(y) such that
R[e; x; y]
unless loc(e) \mmember{} failset ==
(\mforall{}e:E(Y). ((loc(e) \mmember{} locs) \mwedge{} (\mexists{}e':E(X). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)]))))
\mwedge{} (\mforall{}e':E(X)
((\mforall{}i\mmember{}locs.\mexists{}e:E(Y). ((loc(e) = i) \mwedge{} e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)])) \mvee{} (loc(e') \mmember{} failset)))
Date html generated:
2016_05_17-AM-08_18_30
Last ObjectModification:
2012_07_16-AM-10_32_51
Theory : event-ordering
Home
Index