Nuprl Definition : nysiad_add_to_bag

nysiad_add_to_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;waitingmap;mf;...) ==
  λslf,zb,z. let msg,s,d = zb in 
            let msgs,w = z 
            in let m = msg2m msg in
                let f = map-sig-find(waitingmap) d w in
                if isl(f)
                then if deqM outl(f) m then <msgs, map-sig-remove(waitingmap) d w> else <[<m, s, d> / msgs], w> fi 
                else <[<m, s, d> / msgs], w>
                fi 


Definitions occuring in Statement :  cons: [a / b],  outl: outl(x),  ifthenelse: if b then t else f fi ,  isl: isl(x),  let: let,  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>
FDL editor aliases :  nysiad_add_to_bag
Latex:
nysiad\_add\_to\_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;...;...;...;mf;...)  ==
    \mlambda{}slf,zb,z.  let  msg,s,d  =  zb  in 
                        let  msgs,w  =  z 
                        in  let  m  =  msg2m  msg  in
                                let  f  =  map-sig-find(waitingmap)  d  w  in
                                if  isl(f)
                                then  if  deqM  outl(f)  m
                                          then  <msgs,  map-sig-remove(waitingmap)  d  w>
                                          else  <[<m,  s,  d>  /  msgs],  w>
                                          fi 
                                else  <[<m,  s,  d>  /  msgs],  w>
                                fi 


Date html generated: 2016_05_17-PM-01_23_49
Last ObjectModification: 2014_08_06-PM-03_29_44

Theory : event-logic-applications


Home Index