Nuprl Definition : es-first-at-since'
es-first-at-since'(es;i;e;e.R[e];e.P[e]) ==
(loc(e) = i ∈ Id) ∧ R[e] ∧ (∃e':E. ((e' <loc e) c∧ (P[e'] ∧ (∀e'':E. (e' ≤loc e'' ⇒ (e'' <loc e) ⇒ (¬R[e'']))))))
Definitions occuring in Statement :
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-loc: loc(e),
es-E: E,
Id: Id,
cand: A c∧ B,
all: ∀x:A. B[x],
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{} R[e]
\mwedge{} (\mexists{}e':E. ((e' <loc e) c\mwedge{} (P[e'] \mwedge{} (\mforall{}e'':E. (e' \mleq{}loc e'' {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}R[e'']))))))
Date html generated:
2015_07_17-AM-08_50_29
Last ObjectModification:
2013_03_25-PM-01_50_54
Home
Index