Theorem One
LAMPORT, P. 8 — §2.1If $B1(\mathcal{B}$), $B2(\mathcal{B}$), and $B3(\mathcal{B}$) hold, then
(($B_{\text{qrm}}$ $\subseteq$ $B_{\text{vote}}$) $\wedge$ ($B'$qrm $\subseteq$ $B'_\text{vote}))$ $\Rightarrow$ ($B'_{\text{dec}}$ = $B_{\text{dec}}$)
for any $B$, $B'$ in $\mathcal{B}$
LAMPORT, P. 8 — §2.1If $B'_{\text{bal}}$ = $B_{\text{bal}}$ , then $B1(\mathcal{B})$ implies $B'$ = $B$.
If $B'_{\text{bal}}$ $\neq$ $B_{\text{bal}}$ , then the theorem follows immediately from the lemma.
Assume the constraints B1(𝓑), B2(𝓑), and B3(𝓑) hold. Suppose two ballots $B$ and $B'$ satisfy that their quorums are subsets of their votes.
- If $B'_{\mathrm{bal}} = B_{\mathrm{bal}}$, then B1 implies $B' = B$ (they are the same ballot).
- If $B'_{\mathrm{bal}} \neq B_{\mathrm{bal}}$, then the lemma ensures $B'_{\mathrm{dec}} = B_{\mathrm{dec}}$.
Thus, in all cases, the two ballots agree on the decree/value. This proves Theorem One. Either it's the same ballot, or by the lemma a null vote. Hence safety is guaranteed