|
|
|---|
|
|
|
|---|
Establishment of the invariant: the invariant holds in any initial state.
The last committed round is initially 0, so the proof is trivial.
Theorem:
(defthm last-anchor-voters-p-when-init (implies (system-initp systate) (last-anchor-voters-p systate)))