Nuprl Definition : nysiad_query

nysiad_query(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) ==
  λloc,slf,zf,z. let m,s,d = zf in 
                let queue,waiting = z 
                in if loc = d
                   then if isl(s)
                        then if ¬bwaiting
                             then {nysiad_addwaiting'send(add2baghdr;addwaitinghdr;adeliverhdr;...;...;readyhdr;...;mf) 
                                   slf 
                                   hd(queue @ [<m, s, d>])}
                             else {}
                             fi 
                        else {nysiad_adeliver'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;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),  nysiad_addwaiting'send: nysiad_addwaiting'send(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),  eq_id: a = b,  hd: hd(l),  append: as @ bs,  cons: [a / b],  nil: [],  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  isl: isl(x),  spreadn: spread3,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  nysiad_query
Latex:
nysiad\_query(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf)  ==
    \mlambda{}loc,slf,zf,z.  let  m,s,d  =  zf  in 
                                let  queue,waiting  =  z 
                                in  if  loc  =  d
                                      then  if  isl(s)
                                                then  if  \mneg{}\msubb{}waiting
                                                          then  \{nysiad\_addwaiting'send(add2baghdr;...;...;...;...;...;...;mf) 
                                                                      slf 
                                                                      hd(queue  @  [<m,  s,  d>])\}
                                                          else  \{\}
                                                          fi 
                                                else  \{nysiad\_adeliver'send(add2baghdr;addwaitinghdr;...;...;...;...;...;mf) 
                                                            slf 
                                                            <d,  m>\}
                                                fi 
                                      else  \{\}
                                      fi 


Date html generated: 2015_07_23-PM-03_46_26
Last ObjectModification: 2014_08_06-PM-03_33_59

Home Index