local-program-at{i:l}(Info;A;X;dfp;x) ==
(df-program-type(dfp) = A)
(
es:EO+(Info). e:E.
((loc(e) = x)
((X es e)
= last(data-stream(df-program-meaning(
dfp);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,
df-program-meaning: df-program-meaning(dfp),
df-program-type: df-program-type(dfp),
data-stream: data-stream(P;L),
Id: Id,
map: map(f;as),
all: x:A. B[x],
implies: P Q,
and: P Q,
apply: f a,
lambda: x.A[x],
universe: Type,
equal: s = t,
last: last(L),
bag: bag(T)
Definitions :
and: P Q,
universe: Type,
df-program-type: df-program-type(dfp),
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),
df-program-meaning: df-program-meaning(dfp),
map: map(f;as),
lambda: x.A[x],
es-info: info(e),
es-le-before: loc(e)
FDL editor aliases :
local-program-at
local-program-at\{i:l\}(Info;A;X;dfp;x) ==
(df-program-type(dfp) = A)
\mwedge{} (\mforall{}es:EO+(Info). \mforall{}e:E.
((loc(e) = x)
{}\mRightarrow{} ((X es e) = last(data-stream(df-program-meaning(dfp);map(\mlambda{}e.info(e);\mleq{}loc(e)))))))
Date html generated:
2011_08_16-PM-06_14_43
Last ObjectModification:
2011_06_13-PM-03_40_39
Home
Index