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: 2016_05_17-PM-01_05_20
Last ObjectModification: 2014_08_20-PM-00_03_52

Theory : event-logic-applications


Home Index