|
|
|---|
|
|
|
|---|
Invariant that the quorum number does not change.
As proved in the invariant that validator addresses do not change, the set of all, correct, and faulty validators is not changed by state transitions. Consequently, the number of all, correct, and faulty validators is not changed by state transitions. In particular, the maximum number of faulty validators, which is defined from the total number of validators, is not changed by state transitions. And therefore the quorum number, defined as the difference between the total number of validators and the quorum number, is not changed by state transitions.
This is a transition invariant, i.e. it relates the old and new states of transitions.