Nuprl Definition : ohc_v2_Voter
ohc_v2_Voter(Cmd;cmdeq;flrs;learners;locs) ==
zm.let n,c = zm
in (ohc_v2_Phase1(Cmd;cmdeq;flrs;learners;locs) <<n, 0>, c>
|| ohc_v2_NewRounds(Cmd) n >z> ohc_v2_Phase1(Cmd;cmdeq;flrs;learners;locs) z until ohc_v2_Halt() n)
Definitions occuring in Statement :
ohc_v2_Halt: ohc_v2_Halt(),
ohc_v2_NewRounds: ohc_v2_NewRounds(Cmd),
ohc_v2_Phase1: ohc_v2_Phase1(Cmd;cmdeq;flrs;learners;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 :
ohc_v2_Voter
ohc\_v2\_Voter(Cmd;cmdeq;flrs;learners;locs) ==
\mlambda{}zm.let n,c = zm
in (ohc\_v2\_Phase1(Cmd;cmdeq;flrs;learners;locs) <<n, 0>, c>
|| ohc\_v2\_NewRounds(Cmd) n >z> ohc\_v2\_Phase1(Cmd;cmdeq;flrs;learners;locs)
z until ohc\_v2\_Halt() n)
Date html generated:
2012_02_20-PM-05_50_47
Last ObjectModification:
2012_02_17-PM-10_24_54
Home
Index