|
|
|---|
|
|
|
|---|
Establishment of the invariant: the invariant holds in any initial system state.
Initially, there are no signed certificates, so the invariant trivially holds.
Theorem:
(defthm signer-records-p-when-init (implies (system-initp systate) (signer-records-p systate)))