Nuprl Definition : nysiad_on_addwaiting

nysiad_on_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m) ==
  λslf,zc,z. let m,s,d = zc in 
            let msgs,w = z 
            in let f = map-sig-find(waitingmap) d w in
                   if isl(f)
                   then if deqM outl(f) (msg2m m)
                        then {nysiad_ready'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...;mf) 
                              slf 
                              d}
                        else {}
                        fi 
                   else {}
                   fi 


Definitions occuring in Statement :  nysiad_ready'send: nysiad_ready'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),  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,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  nysiad_on_addwaiting
Latex:
nysiad\_on\_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;readyhdr;...;...;mf;...)  ==
    \mlambda{}slf,zc,z.  let  m,s,d  =  zc  in 
                        let  msgs,w  =  z 
                        in  let  f  =  map-sig-find(waitingmap)  d  w  in
                                      if  isl(f)
                                      then  if  deqM  outl(f)  (msg2m  m)
                                                then  \{nysiad\_ready'send(add2baghdr;addwaitinghdr;...;...;...;...;...;mf) 
                                                            slf 
                                                            d\}
                                                else  \{\}
                                                fi 
                                      else  \{\}
                                      fi 


Date html generated: 2016_05_17-PM-01_25_13
Last ObjectModification: 2014_08_06-PM-03_30_45

Theory : event-logic-applications


Home Index