Nuprl Definition : nysiad_InputQueue
nysiad_InputQueue(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
(λslf,x. {inl x} o nysiad_kdeliver'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf))
|| (λslf,x. {inr x } o nysiad_ready'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf)\000C)
Definitions occuring in Statement :
nysiad_kdeliver'base: nysiad_kdeliver'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_ready'base: nysiad_ready'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
parallel-class: X || Y,
eclass0: (f o X),
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
single-bag: {x}
FDL editor aliases :
nysiad_InputQueue
Latex:
nysiad\_InputQueue(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf) ==
(\mlambda{}slf,x. \{inl x\} o nysiad\_kdeliver'base(add2baghdr;addwaitinghdr;adeliverhdr;...;...;readyhdr;...;\000Cmf))
|| (\mlambda{}slf,x. \{inr x \} o nysiad\_ready'base(add2baghdr;addwaitinghdr;adeliverhdr;...;...;readyhdr;...\000C;mf))
Date html generated:
2015_07_23-PM-03_46_00
Last ObjectModification:
2014_08_06-PM-03_33_22
Home
Index