Nuprl Definition : es-happened-before
e1 ⟶ e2 ==
fix((λes-happened-before,e2. ∃e:E
((e < e2)
∧ ((¬(loc(e) = loc(e2) ∈ Id)) ⇒ e2 caused by e in S)
∧ ((e = e1 ∈ E) ∨ (es-happened-before e)))))
e2
Definitions occuring in Statement :
event-caused-by: e2 caused by e1 in S,
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
equal: s = t ∈ T
FDL editor aliases :
es-happened-before
Latex:
e1 {}\mrightarrow{} e2 ==
fix((\mlambda{}es-happened-before,e2. \mexists{}e:E
((e < e2)
\mwedge{} ((\mneg{}(loc(e) = loc(e2))) {}\mRightarrow{} e2 caused by e in S)
\mwedge{} ((e = e1) \mvee{} (es-happened-before e)))))
e2
Date html generated:
2016_05_17-AM-09_04_18
Last ObjectModification:
2013_03_08-PM-00_47_21
Theory : messages
Home
Index