|
|
|---|
|
|
|
|---|
Establishment of the invariant: the invariant holds in any initial state.
Initially the committed anchors are the same (both empty), so they clearly do not fork. The proof does not even depend on their emptiness, just their equality, since both validators' states is validator-init.
Theorem:
(defthm nonforking-anchors-p-when-init (implies (system-initp systate) (nonforking-anchors-p systate)))