Nuprl Definition : nysiad_deliver_to_replica

nysiad_deliver_to_replica(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
  λloc,slf,d,z.
               let queue,waiting = z 
               in if loc = d
                  then if null(queue)
                       then {}
                       else let m',s',d' = hd(queue) in 
                            {nysiad_adeliver'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;mf) 
                             slf 
                             <d', m'>}
                       fi 
                  else {}
                  fi 


Definitions occuring in Statement :  nysiad_adeliver'send: nysiad_adeliver'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),  eq_id: a = b,  hd: hd(l),  null: null(as),  ifthenelse: if b then t else f fi ,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  nysiad_deliver_to_replica
Latex:
nysiad\_deliver\_to\_replica(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;mf)  ==
    \mlambda{}loc,slf,d,z.
                              let  queue,waiting  =  z 
                              in  if  loc  =  d
                                    then  if  null(queue)
                                              then  \{\}
                                              else  let  m',s',d'  =  hd(queue)  in 
                                                        \{nysiad\_adeliver'send(add2baghdr;addwaitinghdr;...;...;...;...;...;mf) 
                                                          slf 
                                                          <d',  m'>\}
                                              fi 
                                    else  \{\}
                                    fi 


Date html generated: 2015_07_23-PM-03_46_16
Last ObjectModification: 2014_08_06-PM-03_33_46

Home Index