		Search-engine friendly clone of the ACL2 documentation.

Backward-closure

Backward-closed-p

Definition of the invariant: the DAG of each correct validator is backward-closed.

Definitions and Theorems

Theorem: backward-closed-p-necc

(defthm backward-closed-p-necc
 (implies
  (backward-closed-p systate)
  (implies
   (in val (correct-addresses systate))
   (dag-closedp
        (validator-state->dag (get-validator-state val systate))))))

Theorem: booleanp-of-backward-closed-p

(defthm booleanp-of-backward-closed-p
  (b* ((yes/no (backward-closed-p systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: backward-closed-p-of-system-state-fix-systate

(defthm backward-closed-p-of-system-state-fix-systate
  (equal (backward-closed-p (system-state-fix systate))
         (backward-closed-p systate)))

Theorem: backward-closed-p-system-state-equiv-congruence-on-systate

(defthm backward-closed-p-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (backward-closed-p systate)
                  (backward-closed-p systate-equiv)))
  :rule-classes :congruence)