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
es-seq(es;S) == \mforall{}e1,e2:E. (e1 before e2 \mmember{} S {}\mRightarrow{} (\mneg{}(e2 < e1)))
Date html generated:
2015_07_17-AM-08_57_32
Last ObjectModification:
2013_03_25-PM-01_53_39
Home
Index