collect-event(es;X;n;v.num[v];L.P[L];e) ==
(
e 
X)
(num[X(e)] = n)
(P[mapfilter(
e.X(e);e.(num[X(e)] =
n);
(X)(e))])
Definitions :
in-eclass: e X,
and: P Q,
equal: s = t,
int: 
,
assert: b,
mapfilter: mapfilter(f;P;L),
lambda: x.A[x],
eq_int: (i = j),
eclass-val: X(e),
es-interface-predecessors: (X)(e)
FDL editor aliases :
collect-event
collect-event(es;X;n;v.num[v];L.P[L];e) ==
(\muparrow{}e \mmember{}\msubb{} X) \mwedge{} (num[X(e)] = n) \mwedge{} (\muparrow{}P[mapfilter(\mlambda{}e.X(e);\mlambda{}e.(num[X(e)] =\msubz{} n);\mleq{}(X)(e))])
Date html generated:
2010_08_27-PM-02_51_39
Last ObjectModification:
2010_03_25-AM-10_18_06
Home
Index