Nuprl Definition : es-first-at-since

es-first-at-since(es;i;e;e.R[e];e.P[e]) ==
  (loc(e) i ∈ Id) ∧ (P[e] ∧ R[e])) ∧ ∀e'<e.P[e']  (∃e'':E. (e' ≤loc e''  ∧ (e'' <loc e) ∧ R[e'']))



Definitions occuring in Statement :  alle-lt: e<e'.P[e] es-le: e ≤loc e'  es-locl: (e <loc e') es-loc: loc(e) es-E: E Id: Id exists: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q equal: t ∈ T
FDL editor aliases :  es-first-at-since es-first-at-since

Latex:
es-first-at-since(es;i;e;e.R[e];e.P[e])  ==
    (loc(e)  =  i)  \mwedge{}  (P[e]  \mwedge{}  (\mneg{}R[e]))  \mwedge{}  \mforall{}e'<e.P[e']  {}\mRightarrow{}  (\mexists{}e'':E.  (e'  \mleq{}loc  e''    \mwedge{}  (e''  <loc  e)  \mwedge{}  R[e'']))



Date html generated: 2016_05_16-AM-09_49_38
Last ObjectModification: 2013_03_25-PM-01_50_52

Theory : new!event-ordering


Home Index