Nuprl Definition : nysiad_on_add2bag

nysiad_on_add2bag(M;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;senders;...;waitingmap;mf) ==
  λslf,zd,z. let m,s,d = zd in 
            let msgs,w = z 
            in if d = slf
               then nysiad_tooarcast'broadcast(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...;mf) 
                    senders 
                    <m, s, d>
               else {}
               fi 


Definitions occuring in Statement :  nysiad_tooarcast'broadcast: nysiad_tooarcast'broadcast(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),  eq_id: a = b,  ifthenelse: if b then t else f fi ,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  empty-bag: {}
FDL editor aliases :  nysiad_on_add2bag
Latex:
nysiad\_on\_add2bag(M;add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;...;...;mf)  ==
    \mlambda{}slf,zd,z.  let  m,s,d  =  zd  in 
                        let  msgs,w  =  z 
                        in  if  d  =  slf
                              then  nysiad\_tooarcast'broadcast(add2baghdr;addwaitinghdr;...;...;...;...;...;mf) 
                                        senders 
                                        <m,  s,  d>
                              else  \{\}
                              fi 


Date html generated: 2016_05_17-PM-01_25_29
Last ObjectModification: 2014_08_06-PM-03_30_56

Theory : event-logic-applications


Home Index