Nuprl Definition : nysiad_on_addwaiting
nysiad_on_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m) ==
λslf,zc,z. let m,s,d = zc in
let msgs,w = z
in let f = map-sig-find(waitingmap) d w in
if isl(f)
then if deqM outl(f) (msg2m m)
then {nysiad_ready'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;mf)
slf
d}
else {}
fi
else {}
fi
Definitions occuring in Statement :
nysiad_ready'send: nysiad_ready'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
outl: outl(x),
ifthenelse: if b then t else f fi ,
isl: isl(x),
let: let,
spreadn: spread3,
apply: f a,
lambda: λx.A[x],
spread: spread def,
single-bag: {x},
empty-bag: {},
map-sig-find: map-sig-find(m)
FDL editor aliases :
nysiad_on_addwaiting
Latex:
nysiad\_on\_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;readyhdr;...;...;mf;...) ==
\mlambda{}slf,zc,z. let m,s,d = zc in
let msgs,w = z
in let f = map-sig-find(waitingmap) d w in
if isl(f)
then if deqM outl(f) (msg2m m)
then \{nysiad\_ready'send(add2baghdr;addwaitinghdr;...;...;...;...;...;mf)
slf
d\}
else \{\}
fi
else \{\}
fi
Date html generated:
2015_07_23-PM-03_44_08
Last ObjectModification:
2014_08_06-PM-03_30_45
Home
Index