X <-- Z ==
e':E. v:T. (v 
X(e') 
(
e:E. ((e < e') 
<loc(e'), info(e')> Z(e))))
Definitions occuring in Statement :
Message: Message,
classrel: v X(e),
es-info: info(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
X <-- Z == \mforall{}e':E. \mforall{}v:T. (v \mmember{} X(e') {}\mRightarrow{} (\mdownarrow{}\mexists{}e:E. ((e < e') \mwedge{} <loc(e'), info(e')> \mmember{} Z(e))))
Date html generated:
2011_08_17-PM-04_05_15
Last ObjectModification:
2011_07_20-PM-08_01_29
Home
Index