Nuprl Definition : RSC_VoterState

RSC_VoterState(Cmd) ==
  z.Accum-class(v,state.
                  if RSC_round_increase() z v state then RSC_incround() v state else state fi ;RSC_init() 
                                                                                               0;RSC_RoundInfo(Cmd))


Definitions occuring in Statement :  RSC_incround: RSC_incround(),  RSC_round_increase: RSC_round_increase(),  RSC_RoundInfo: RSC_RoundInfo(Cmd),  RSC_init: RSC_init(),  Accum-class: Accum-class(f;init;X),  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: x.A[x],  natural_number: $n
FDL editor aliases :  RSC_VoterState
RSC\_VoterState(Cmd)  ==
    \mlambda{}z.Accum-class(\mlambda{}v,state.
                                    if  RSC\_round\_increase()  z  v  state
                                    then  RSC\_incround()  v  state
                                    else  state
                                    fi  ;RSC\_init()  0;RSC\_RoundInfo(Cmd))


Date html generated: 2012_02_20-PM-04_01_40
Last ObjectModification: 2012_02_02-PM-01_59_24

Home Index