LProgrammable(A;X) ==
i:Id
df:dataflow(Info;bag(A))
es:EO+(Info). e:E.
((loc(e) = i)
((X es e) = last(data-stream(df;map(
e.info(e);
loc(e))))))
Definitions occuring in Statement :
es-info: info(e),
event-ordering+: EO+(Info),
es-le-before: loc(e),
es-loc: loc(e),
es-E: E,
data-stream: data-stream(P;L),
dataflow: dataflow(A;B),
Id: Id,
map: map(f;as),
all: x:A. B[x],
exists: x:A. B[x],
implies: P Q,
apply: f a,
lambda: x.A[x],
equal: s = t,
last: last(L),
bag: bag(T)
Definitions :
exists: x:A. B[x],
dataflow: dataflow(A;B),
event-ordering+: EO+(Info),
all: x:A. B[x],
es-E: E,
implies: P Q,
Id: Id,
es-loc: loc(e),
equal: s = t,
bag: bag(T),
apply: f a,
last: last(L),
data-stream: data-stream(P;L),
map: map(f;as),
lambda: x.A[x],
es-info: info(e),
es-le-before: loc(e)
FDL editor aliases :
locally-programmable
LProgrammable(A;X) ==
\mforall{}i:Id
\mexists{}df:dataflow(Info;bag(A))
\mforall{}es:EO+(Info). \mforall{}e:E.
((loc(e) = i) {}\mRightarrow{} ((X es e) = last(data-stream(df;map(\mlambda{}e.info(e);\mleq{}loc(e))))))
Date html generated:
2011_08_16-PM-06_14_19
Last ObjectModification:
2011_06_13-PM-01_11_46
Home
Index