ESMachineAxiom(E;T;V;M;loc;knd;val;
when;after;
sndr;Trans;Send;Choose) ==
(
e:E. ((
x.(after x e)) = (Trans (loc e) (knd e) (val e) (x.(when x e)))))
(e:E
((
islocal(knd e))
((isl(Choose (loc e) act(knd e) (x.(when x e))))
c ((val e) = outl(Choose (loc e) act(knd e) (x.(when x e)))))))
(e:E
((isrcv(knd e))
(<lnk(knd e), tag(knd e), val e> 
Send (loc (sndr e)) (knd (sndr e))
(val (sndr e))
(x.(when x (sndr e))))))
Definitions :
function: x:A 
B[x],
Id: Id,
and: P Q,
islocal: islocal(k),
cand: A c B,
isl: isl(x),
equal: s = t,
outl: outl(x),
actof: act(k),
all: x:A. B[x],
implies: P Q,
assert: b,
isrcv: isrcv(k),
l_member: (x l),
lnk: lnk(k),
pair: <a, b>,
tagof: tag(k),
lambda: x.A[x],
apply: f a,
Msg: Msg(M)
FDL editor aliases :
ESMachineAxiom
ESMachineAxiom(E;T;V;M;loc;knd;val;
when;after;
sndr;Trans;Send;Choose) ==
(\mforall{}e:E. ((\mlambda{}x.(after x e)) = (Trans (loc e) (knd e) (val e) (\mlambda{}x.(when x e)))))
\mwedge{} (\mforall{}e:E
((\muparrow{}islocal(knd e))
{}\mRightarrow{} ((\muparrow{}isl(Choose (loc e) act(knd e) (\mlambda{}x.(when x e))))
c\mwedge{} ((val e) = outl(Choose (loc e) act(knd e) (\mlambda{}x.(when x e)))))))
\mwedge{} (\mforall{}e:E
((\muparrow{}isrcv(knd e))
{}\mRightarrow{} (<lnk(knd e), tag(knd e), val e> \mmember{} Send (loc (sndr e)) (knd (sndr e)) (val (sndr e))
(\mlambda{}x.(when x (sndr e))))))
Date html generated:
2010_08_27-AM-01_08_11
Last ObjectModification:
2009_12_16-AM-12_38_06
Home
Index