Nuprl Definition : es-quiet-until

es-quiet-until(es;i;e.P[e]) ==
  ∃e:E. ((loc(e) i ∈ Id) ∧ (∀e':E. ((¬(loc(e') i ∈ Id))  (e < e')  (∃e'':E. ((e'' < e') ∧ P[e''])))))



Definitions occuring in Statement :  es-causl: (e < e') es-loc: loc(e) es-E: E Id: Id all: x:A. B[x] exists: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q equal: t ∈ T
FDL editor aliases :  es-quiet-until es-quiet-until

Latex:
es-quiet-until(es;i;e.P[e])  ==
    \mexists{}e:E.  ((loc(e)  =  i)  \mwedge{}  (\mforall{}e':E.  ((\mneg{}(loc(e')  =  i))  {}\mRightarrow{}  (e  <  e')  {}\mRightarrow{}  (\mexists{}e'':E.  ((e''  <  e')  \mwedge{}  P[e''])))))



Date html generated: 2016_05_16-AM-10_36_09
Last ObjectModification: 2013_03_25-PM-01_59_37

Theory : new!event-ordering


Home Index