Constraints

Ballot Uniqueness

$\mathbf{B1}(\mathcal{B})$: $\triangleq \forall B, B' \in \mathcal{B} : (B \neq B') \Rightarrow (B_{\text{bal}} \neq B'_{\text{bal}})$

If two distinct ballots $B$ and $B'$ belong to the set $\mathcal{B}$, then their ballot numbers $B_{\text{bal}}$ and $B'_{\text{bal}}$ must also be distinct.

Quorums

$\mathbf{B2}(\mathcal{B})$: $\triangleq \forall B, B' \in \mathcal{B}$ : $B_{\text{qrm}}$ $\cap$ $B'_{\text{qrm}}$ $\neq$ $\emptyset$

For any two ballots $B$ and $B'$ in the set $\mathcal{B}$, their quorums $B_{\text{qrm}}$ and $B'_{\text{qrm}}$ must have at least one node in common; i.e., their intersection is not empty.

Decree Consistency

$\mathbf{B3}(\mathcal{B})$: $\triangleq \forall B \in \mathcal{B} : (\text{MaxVote}(B_{\text{bal}}, B_{\text{qrm}}, \mathcal{B})_{\text{bal}} = -\infty) \Rightarrow (B_{\text{dec}} = \text{MaxVote}(B_{\text{bal}}, B_{\text{qrm}}, \mathcal{B})_{\text{dec}})$

For any ballot $B$ in the set $\mathcal{B}$, if there is no previously accepted ballot in the quorum with a higher ballot number, then the value $B_{\text{dec}}$ of $B$ must match the value of the highest previously accepted ballot (if any). In other words, a ballot cannot choose a overwrite or contradicts a previously accepted value in its quorum.