Nuprl Definition : OARcast_orderer_for_sender_outputs
OARcast_orderer_for_sender_outputs(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) ==
λsndr,slf,z. let seqms,z = z
in bag-union(map(λseqm.(OARcast_ordered'bsign(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) receivers
<slf, sndr, seqm>);seqms))
Definitions occuring in Statement :
OARcast_ordered'bsign: OARcast_ordered'bsign(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
,
map: map(f;as)
,
apply: f a
,
lambda: λx.A[x]
,
spread: spread def,
pair: <a, b>
,
bag-union: bag-union(bbs)
FDL editor aliases :
OARcast_orderer_for_sender_outputs
Latex:
OARcast\_orderer\_for\_sender\_outputs(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;receivers;mf) ==
\mlambda{}sndr,slf,z. let seqms,z = z
in bag-union(
map(\mlambda{}seqm.(OARcast\_ordered'bsign(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf)
receivers
<slf, sndr, seqm>);seqms))
Date html generated:
2015_07_23-PM-00_31_34
Last ObjectModification:
2014_08_20-PM-00_03_52
Home
Index