Nuprl Definition : es-seq

es-seq(es;S) ==  ∀e1,e2:E.  (e1 before e2 ∈  (e2 < e1)))



Definitions occuring in Statement :  es-causl: (e < e') es-E: E l_before: before y ∈ l all: x:A. B[x] not: ¬A implies:  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