|
|
|---|
|
|
|
|---|
Preservation of the invariant by multiple transitions.
Theorem:
(defthm ordered-blockchain-p-of-events-next (implies (and (events-possiblep events systate) (last-blockchain-round-p systate) (ordered-blockchain-p systate)) (ordered-blockchain-p (events-next events systate))))