Nuprl Definition : RSC_Voter

RSC_Voter(Cmd;clients;cmdeq;flrs;locs) ==
  zn.let n,c = zn 
      in RSC_Round(Cmd;cmdeq;flrs;locs) <<n, 0>, c> || RSC_Notify(Cmd;clients) n
         || (RSC_NewRounds(Cmd) n >z> RSC_Round(Cmd;cmdeq;flrs;locs) z until RSC_Notify(Cmd;clients) n)


Definitions occuring in Statement :  RSC_Notify: RSC_Notify(Cmd;clients),  RSC_NewRounds: RSC_NewRounds(Cmd),  RSC_Round: RSC_Round(Cmd;cmdeq;flrs;locs),  until-class: (X until Y),  parallel-class: X || Y,  bind-class: X >x> Y[x],  apply: f a,  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  natural_number: $n
FDL editor aliases :  RSC_Voter
RSC\_Voter(Cmd;clients;cmdeq;flrs;locs)  ==
    \mlambda{}zn.let  n,c  =  zn 
            in  RSC\_Round(Cmd;cmdeq;flrs;locs)  <<n,  0>,  c>  ||  RSC\_Notify(Cmd;clients)  n
                  ||  (RSC\_NewRounds(Cmd)  n  >z>  RSC\_Round(Cmd;cmdeq;flrs;locs) 
                                                                            z  until  RSC\_Notify(Cmd;clients)  n)


Date html generated: 2012_02_20-PM-03_59_52
Last ObjectModification: 2012_02_02-PM-01_58_41

Home Index