Nuprl Definition : es-class-causal-rel
e∈X(x) ⇐c⇒ Y(y) such that
R[e; x; y] ==
(∀e:E(Y). ∃e':E(X). (e' c≤ e ∧ R[e'; X(e'); Y(e)])) ∧ (∀e':E(X). ∃e:E(Y). (e' c≤ e ∧ R[e'; X(e'); Y(e)]))
Definitions occuring in Statement :
es-E-interface: E(X),
eclass-val: X(e),
es-causle: e c≤ e',
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
and: P ∧ Q
FDL editor aliases :
es-class-causal-rel
Latex:
e\mmember{}X(x) \mLeftarrow{}c\mRightarrow{} Y(y) such that
R[e; x; y] ==
(\mforall{}e:E(Y). \mexists{}e':E(X). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)]))
\mwedge{} (\mforall{}e':E(X). \mexists{}e:E(Y). (e' c\mleq{} e \mwedge{} R[e'; X(e'); Y(e)]))
Date html generated:
2016_05_17-AM-08_15_01
Last ObjectModification:
2012_02_25-PM-03_15_00
Theory : event-ordering
Home
Index