Nuprl Definition : onethird-consensus
onethird-consensus(es;t;Input;Vote;Output;voters;clients) ==
no_repeats(Id;voters)
∧ (||voters|| = ((3 * t) + 1) ∈ ℤ)
∧ left(inning_val()[es-threshold(es; simple_consensus_init(); inning_step(); inning_test(1); nxt_inning(); Input+Vote
)])
⇐⇒ Vote@voters
∧ right(inning_val()[es-threshold(es; simple_consensus_init(); inning_step(); inning_test(1); nxt_inning(); Input+Vote
)])
⇐⇒ Output@clients
Definitions occuring in Statement :
Id: Id
,
no_repeats: no_repeats(T;l)
,
length: ||as||
,
nat: ℕ
,
and: P ∧ Q
,
product: x:A × B[x]
,
multiply: n * m
,
add: n + m
,
natural_number: $n
,
int: ℤ
,
equal: s = t ∈ T
FDL editor aliases :
onethird-consensus
onethird-consensus
onethird-consensus(es;t;Input;Vote;Output;voters;clients) ==
no\_repeats(Id;voters)
\mwedge{} (||voters|| = ((3 * t) + 1))
\mwedge{} left(inning\_val()[es-threshold(es;
simple\_consensus\_init();
inning\_step();
inning\_test(1);
nxt\_inning();
Input+Vote)]) \mLeftarrow{}{}\mRightarrow{} Vote@voters
\mwedge{} right(inning\_val()[es-threshold(es;
simple\_consensus\_init();
inning\_step();
inning\_test(1);
nxt\_inning();
Input+Vote)]) \mLeftarrow{}{}\mRightarrow{} Output@clients
Date html generated:
2015_07_17-AM-09_05_23
Last ObjectModification:
2013_03_25-PM-01_56_50
Home
Index