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