Nuprl Definition : ohc_v1_Voter
ohc_v1_Voter(Cmd;cmdeq;flrs;learners;locs) ==
zm.let n,c = zm
in (ohc_v1_Phase1(Cmd;cmdeq;flrs;learners;locs) <<n, 0>, c>
|| ohc_v1_NewRounds(Cmd) n >z> ohc_v1_Phase1(Cmd;cmdeq;flrs;learners;locs) z until ohc_v1_Halt() n)
Definitions occuring in Statement :
ohc_v1_Halt: ohc_v1_Halt(),
ohc_v1_NewRounds: ohc_v1_NewRounds(Cmd),
ohc_v1_Phase1: ohc_v1_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_v1_Voter
ohc\_v1\_Voter(Cmd;cmdeq;flrs;learners;locs) ==
\mlambda{}zm.let n,c = zm
in (ohc\_v1\_Phase1(Cmd;cmdeq;flrs;learners;locs) <<n, 0>, c>
|| ohc\_v1\_NewRounds(Cmd) n >z> ohc\_v1\_Phase1(Cmd;cmdeq;flrs;learners;locs)
z until ohc\_v1\_Halt() n)
Date html generated:
2012_02_20-PM-05_26_09
Last ObjectModification:
2012_02_13-PM-12_58_25
Home
Index