Nuprl Definition : nysiad_MessageBagInput
nysiad_MessageBagInput(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
(λslf,x. {inl x} o nysiad_addwaiting'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf\000C))
|| (λslf,x. {inr x } o nysiad_add2bag'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;m\000Cf))
Definitions occuring in Statement :
nysiad_addwaiting'base: nysiad_addwaiting'base(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_add2bag'base: nysiad_add2bag'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_MessageBagInput
Latex:
nysiad\_MessageBagInput(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...;mf) ==
(\mlambda{}slf,x. \{inl x\} o nysiad\_addwaiting'base(add2baghdr;addwaitinghdr;adeliverhdr;...;...;readyhdr;..\000C.;mf))
|| (\mlambda{}slf,x. \{inr x \} o nysiad\_add2bag'base(add2baghdr;addwaitinghdr;adeliverhdr;...;...;...;...;mf\000C))
Date html generated:
2015_07_23-PM-03_44_36
Last ObjectModification:
2014_08_06-PM-03_31_22
Home
Index