Nuprl Definition : nysiad_MessageBagInput-program
nysiad_MessageBagInput-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
eclass0-program(λslf,x. {inl x};
nysiad_addwaiting'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf))
|| eclass0-program(λslf,x. {inr x };
nysiad_add2bag'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf))
Definitions occuring in Statement :
nysiad_addwaiting'base-program: nysiad_addwaiting'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_add2bag'base-program: nysiad_add2bag'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
parallel-class-program: X || Y,
eclass0-program: eclass0-program(f;pr),
lambda: λx.A[x],
inr: inr x ,
inl: inl x,
single-bag: {x}
FDL editor aliases :
nysiad_MessageBagInput-program
Latex:
nysiad\_MessageBagInput-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf) ==
eclass0-program(\mlambda{}slf,x. \{inl x\};
nysiad\_addwaiting'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf))
|| eclass0-program(\mlambda{}slf,x. \{inr x \};
nysiad\_add2bag'base-program(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf))
Date html generated:
2015_07_23-PM-03_44_45
Last ObjectModification:
2014_08_06-PM-03_31_35
Home
Index