Nuprl Definition : OARcast_deliverer_for_sender_seq_output

OARcast_deliverer_for_sender_seq_output(M;deliverhdr;flrs;oarcasthdr;orderedhdr;orderhdr;mf) ==
  λsndr,seq,slf,state. let d = oarcast-deliver-output((2 * flrs) + 1;state) in
                           if isl(d)
                           then {OARcast_deliver'send(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf) slf 
                                 <sndr, seq, outl(d)>}
                           else {}
                           fi 


Definitions occuring in Statement :  OARcast_deliver'send: OARcast_deliver'send(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr;mf),  oarcast-deliver-output: oarcast-deliver-output(num;s),  outl: outl(x),  ifthenelse: if b then t else f fi ,  isl: isl(x),  let: let,  apply: f a,  lambda: λx.A[x],  pair: <a, b>,  multiply: n * m,  add: n + m,  natural_number: $n,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  OARcast_deliverer_for_sender_seq_output
Latex:
OARcast\_deliverer\_for\_sender\_seq\_output(M;deliverhdr;flrs;oarcasthdr;orderedhdr;orderhdr;mf)  ==
    \mlambda{}sndr,seq,slf,state.
                                            let  d  =  oarcast-deliver-output((2  *  flrs)  +  1;state)  in
                                                    if  isl(d)
                                                    then  \{OARcast\_deliver'send(M;deliverhdr;oarcasthdr;orderedhdr;...;mf) 
                                                                slf 
                                                                <sndr,  seq,  outl(d)>\}
                                                    else  \{\}
                                                    fi 


Date html generated: 2015_07_23-PM-00_33_32
Last ObjectModification: 2014_08_20-PM-00_06_31

Home Index