|
|
|---|
|
|
|
|---|
Establishment of the invariant: the invariant holds in any initial system state.
Initially, all DAGs are empty, so the invariant trivially holds.
Theorem:
(defthm unequivocal-dags-p-when-init (implies (system-initp systate) (unequivocal-dags-p systate)))