Nuprl Definition : mu_ex_v4_HandleLeaveCS

mu_ex_v4_HandleLeaveCS(initial_token;proc1;proc2) ==
  l.let F = zl,zk,n,z.
              let interested,token,toreply = z in 
              if toreply then {mu_ex_v4_send_token() (mu_ex_v4_otherProc(proc1;proc2) l) (n + 1)} else {} fi  in
         concat-lifting-loc-3(F)|Loc, mu_ex_v4_LeaveCS(), mu_ex_v4_PrToken(), mu_ex_v4_PrState(initial_token)|


Definitions occuring in Statement :  mu_ex_v4_PrToken: mu_ex_v4_PrToken(),  mu_ex_v4_PrState: mu_ex_v4_PrState(initial_token),  mu_ex_v4_otherProc: mu_ex_v4_otherProc(proc1;proc2),  mu_ex_v4_LeaveCS: mu_ex_v4_LeaveCS(),  mu_ex_v4_send_token: mu_ex_v4_send_token(),  concat-lifting-loc-3: concat-lifting-loc-3(f),  simple-loc-comb-3: F|Loc, X, Y, Z|,  ifthenelse: if b then t else f fi ,  let: let,  spreadn: spread3,  apply: f a,  lambda: x.A[x],  add: n + m,  natural_number: $n,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  mu_ex_v4_HandleLeaveCS
mu\_ex\_v4\_HandleLeaveCS(initial$_{token}$;proc1;proc2)  ==
    \mlambda{}l.let  F  =  \mlambda{}zl,zk,n,z.
                            let  interested,token,toreply  =  z  in 
                            if  toreply
                            then  \{mu\_ex\_v4\_send\_token()  (mu\_ex\_v4\_otherProc(proc1;proc2)  l)  (n  +  1)\}
                            else  \{\}
                            fi    in
                  concat-lifting-loc-3(F)|Loc,  mu\_ex\_v4\_LeaveCS(),  mu\_ex\_v4\_PrToken(),
                  mu\_ex\_v4\_PrState(initial$_{token}$)|


Date html generated: 2012_02_20-PM-06_32_49
Last ObjectModification: 2012_02_02-PM-02_54_02

Home Index