es-first-at-since(es;i;e;e.R[e];e.P[e]) ==
(loc(e) = i)
(P[e] (
R[e]))
e'<e.P[e'] 
(
e'':E. (e' 
loc e'' (e'' <loc e) R[e'']))
Definitions :
equal: s = t,
Id: Id,
es-loc: loc(e),
not: A,
alle-lt: e<e'.P[e],
implies: P Q,
exists: x:A. B[x],
es-E: E,
es-le: e loc e' ,
and: P Q,
es-locl: (e <loc e')
FDL editor aliases :
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:
2010_08_27-AM-09_30_22
Last ObjectModification:
2009_12_16-AM-01_06_19
Home
Index