Nuprl Definition : rsc2_roundout

rsc2_roundout(Cmd;cmdeq;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|| (2 * flrs)
                  then let k,x = poss-maj(cmdeq;[c / cmds];c) 
                       in if IntDeq k ((2 * flrs) + 1)
                          then {rsc2_decided'send(Cmd) loc <n, x>}
                          else {rsc2_retry'send(Cmd) loc <<n, i + 1>, x>}
                          fi 
                  else {}
                  fi 


Definitions occuring in Statement :  rsc2_decided'send: rsc2_decided'send(Cmd),  rsc2_retry'send: rsc2_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 :  rsc2_roundout
rsc2\_roundout(Cmd;cmdeq;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||  (2  *  flrs)
                                    then  let  k,x  =  poss-maj(cmdeq;[c  /  cmds];c) 
                                              in  if  IntDeq  k  ((2  *  flrs)  +  1)
                                                    then  \{rsc2\_decided'send(Cmd)  loc  <n,  x>\}
                                                    else  \{rsc2\_retry'send(Cmd)  loc  <<n,  i  +  1>,  x>\}
                                                    fi 
                                    else  \{\}
                                    fi 


Date html generated: 2012_02_20-PM-04_41_48
Last ObjectModification: 2012_02_02-PM-02_05_29

Home Index