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