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: m add: m natural_number: $n int: equal: t ∈ T
FDL editor aliases :  onethird-consensus onethird-consensus

Latex:
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: 2016_05_16-AM-10_24_17
Last ObjectModification: 2013_03_25-PM-01_56_50

Theory : new!event-ordering


Home Index