Nuprl Definition : new_23_sig_roundout

new_23_sig_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f) ==
  λloc,za,z. let zb,sender = za 
             in let zc,c = zb 
                in let n,i = zc 
                   in let cmds,locs = z 
                      in if (||cmds|| =z coeff * flrs)
                         then let k,x = poss-maj(cmdeq;[c / cmds];c) 
                              in if (k =z (coeff * flrs) + 1)
                                 then new_23_sig_decided'broadcast(Cmd;notify;propose;f) reps <n, x>
                                 else {new_23_sig_retry'send(Cmd;notify;propose;f) loc <<n, i + 1>, x>}
                                 fi 
                         else {}
                         fi 


Definitions occuring in Statement :  new_23_sig_decided'broadcast: new_23_sig_decided'broadcast(Cmd;notify;propose;f),  new_23_sig_retry'send: new_23_sig_retry'send(Cmd;notify;propose;f),  poss-maj: poss-maj(eq;L;x),  length: ||as||,  cons: [a / b],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  multiply: n * m,  add: n + m,  natural_number: $n,  single-bag: {x},  empty-bag: {}
FDL editor aliases :  new_23_sig_roundout
Latex:
new\_23\_sig\_roundout(Cmd;cmdeq;coeff;flrs;notify;propose;reps;f)  ==
    \mlambda{}loc,za,z.  let  zb,sender  =  za 
                          in  let  zc,c  =  zb 
                                in  let  n,i  =  zc 
                                      in  let  cmds,locs  =  z 
                                            in  if  (||cmds||  =\msubz{}  coeff  *  flrs)
                                                  then  let  k,x  =  poss-maj(cmdeq;[c  /  cmds];c) 
                                                            in  if  (k  =\msubz{}  (coeff  *  flrs)  +  1)
                                                                  then  new\_23\_sig\_decided'broadcast(Cmd;notify;propose;f)  reps  <n,  x>
                                                                  else  \{new\_23\_sig\_retry'send(Cmd;notify;propose;f)  loc 
                                                                              <<n,  i  +  1>,  x>\}
                                                                  fi 
                                                  else  \{\}
                                                  fi 


Date html generated: 2015_07_23-PM-03_50_28
Last ObjectModification: 2013_11_23-PM-09_54_40

Home Index