Nuprl Definition : rsc3_roundout

rsc3_roundout(Cmd;cmdeq;coeff;flrs) ==
  loc,za.
   let zb,sender = za 
   in let zc,c = zb 
      in let n,i = zc 
         in z.let cmds,z = z 
               in if IntDeq ||cmds|| (coeff * flrs)
                  then let k,x = poss-maj(cmdeq;[c / cmds];c) 
                       in if IntDeq k ((coeff * flrs) + 1)
                          then {rsc3_decided'send(Cmd) loc <n, x>}
                          else {rsc3_retry'send(Cmd) loc <<n, i + 1>, x>}
                          fi 
                  else {}
                  fi 


Definitions occuring in Statement :  rsc3_decided'send: rsc3_decided'send(Cmd),  rsc3_retry'send: rsc3_retry'send(Cmd),  length: ||as||,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  cons: [car / cdr],  multiply: n * m,  add: n + m,  natural_number: $n,  poss-maj: poss-maj(eq;L;x),  int-deq: IntDeq,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  rsc3_roundout
rsc3\_roundout(Cmd;cmdeq;coeff;flrs)  ==
    \mlambda{}loc,za.
      let  zb,sender  =  za 
      in  let  zc,c  =  zb 
            in  let  n,i  =  zc 
                  in  \mlambda{}z.let  cmds,z  =  z 
                              in  if  IntDeq  ||cmds||  (coeff  *  flrs)
                                    then  let  k,x  =  poss-maj(cmdeq;[c  /  cmds];c) 
                                              in  if  IntDeq  k  ((coeff  *  flrs)  +  1)
                                                    then  \{rsc3\_decided'send(Cmd)  loc  <n,  x>\}
                                                    else  \{rsc3\_retry'send(Cmd)  loc  <<n,  i  +  1>,  x>\}
                                                    fi 
                                    else  \{\}
                                    fi 


Date html generated: 2012_02_20-PM-04_11_37
Last ObjectModification: 2012_02_02-PM-02_03_16

Home Index