|
|
|---|
|
|
|
|---|
Establishment of the invariant: the invariant holds in any initial system state.
Initially all the DAGs are empty, so the universal quantification is trivially true.
Theorem:
(defthm dag-previous-quorum-p-when-init (implies (system-initp systate) (dag-previous-quorum-p systate)))