X <-- p.Z[p] ==
e':E. v:T.
(v 
X(e')
(
e,start:E
p:A. (start 
loc e 
(e < e') <loc(e'), info(e')> Z[p](e))))
Definitions occuring in Statement :
Message: Message,
classrel: v X(e),
eo-forward: eo.e,
es-info: info(e),
es-le: e loc e' ,
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
pair: <a, b>,
product: x:A 
B[x]
FDL editor aliases :
class-caused-by-some
X <-- p.Z[p] ==
\mforall{}e':E. \mforall{}v:T.
(v \mmember{} X(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e,start:E. \mexists{}p:A. (start \mleq{}loc e \mwedge{} (e < e') \mwedge{} <loc(e'), info(e')> \mmember{} Z[p](e))))
Date html generated:
2011_08_17-PM-04_05_33
Last ObjectModification:
2011_07_21-PM-12_51_19
Home
Index