Nuprl Definition : nysiad_Queue-program
nysiad_Queue-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
λloc.eclass1-program(nysiad_on_input_queue(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...;mf)
loc;
nysiad_InputQueue-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;mf))
o nysiad_QueueState-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf)
loc
Definitions occuring in Statement :
nysiad_on_input_queue: nysiad_on_input_queue(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_InputQueue-program: nysiad_InputQueue-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_QueueState-program: nysiad_QueueState-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
eclass2-program: Xpr o Ypr,
eclass1-program: eclass1-program(f;pr),
apply: f a,
lambda: λx.A[x]
FDL editor aliases :
nysiad_Queue-program
Latex:
nysiad\_Queue-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...;mf) ==
\mlambda{}loc.eclass1-program(nysiad\_on\_input\_queue(add2baghdr;addwaitinghdr;...;...;...;readyhdr;...;mf)
loc;
nysiad\_InputQueue-program(add2baghdr;addwaitinghdr;...;...;...;...;...;mf))
o nysiad\_QueueState-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf)
loc
Date html generated:
2015_07_23-PM-03_46_52
Last ObjectModification:
2014_08_06-PM-03_34_35
Home
Index