Nuprl Definition : nysiad_add_waiting

nysiad_add_waiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m) ==
  λslf,za,z. let msg,s,d = za in 
            let msgs,w = z 
            in let m = msg2m msg in
                   if <m, s, d> ∈b msgs)
                   then <remove-first(λx.(product-deq(M;Id?
                                          × Id;deqM;product-deq(Id?;Id;union-deq(Id;Unit;IdDeq;UnitDeq);IdDeq)) 
                                          x 
                                          <m, s, d>);msgs)
                        , w
                        >
                   else <msgs, map-sig-add(waitingmap) d m w>
                   fi 


Definitions occuring in Statement :  nysiad_Amessage-deq: nysiad_Amessage-deq(M;deqM),  id-deq: IdDeq,  Id: Id,  deq-member: x ∈b L),  union-deq: union-deq(A;B;a;b),  product-deq: product-deq(A;B;a;b),  unit-deq: UnitDeq,  remove-first: remove-first(P;L),  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread3,  unit: Unit,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  product: x:A × B[x],  union: left + right,  map-sig-add: map-sig-add(m)
FDL editor aliases :  nysiad_add_waiting
Latex:
nysiad\_add\_waiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;readyhdr;...;...;mf;msg2m)  ==
    \mlambda{}slf,za,z.  let  msg,s,d  =  za  in 
                        let  msgs,w  =  z 
                        in  let  m  =  msg2m  msg  in
                                      if  <m,  s,  d>  \mmember{}\msubb{}  msgs)
                                      then  <remove-first(\mlambda{}x.(product-deq(M;Id?
                                                                                    \mtimes{}  Id;deqM;product-deq(Id?;Id;union-deq(Id;Unit;IdDeq;
                                                                                                                                                                  UnitDeq);IdDeq)) 
                                                                                    x 
                                                                                    <m,  s,  d>);msgs)
                                                ,  w
                                                >
                                      else  <msgs,  map-sig-add(waitingmap)  d  m  w>
                                      fi 


Date html generated: 2015_07_23-PM-03_43_09
Last ObjectModification: 2014_08_06-PM-03_29_32

Home Index