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