Nuprl Definition : es-seq
es-seq(es;S) == ∀e1,e2:E. (e1 before e2 ∈ S ⇒ (¬(e2 < e1)))
Definitions occuring in Statement :
es-causl: (e < e'),
es-E: E,
l_before: x before y ∈ l,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q
FDL editor aliases :
es-seq
es-seq
Latex:
es-seq(es;S) == \mforall{}e1,e2:E. (e1 before e2 \mmember{} S {}\mRightarrow{} (\mneg{}(e2 < e1)))
Date html generated:
2016_05_16-AM-10_04_26
Last ObjectModification:
2013_03_25-PM-01_53_39
Theory : new!event-ordering
Home
Index