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: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
es-first-at-since
es-first-at-since
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:
2015_07_17-AM-08_50_24
Last ObjectModification:
2013_03_25-PM-01_50_52
Home
Index