		Search-engine friendly clone of the ACL2 documentation.

Initialization

System-validators-initp

Check if all the correct validators in the system are in the initial state.

Definitions and Theorems

Theorem: system-validators-initp-necc

(defthm system-validators-initp-necc
  (implies (system-validators-initp systate)
           (implies (in val (correct-addresses systate))
                    (equal (get-validator-state val systate)
                           (validator-init)))))

Theorem: booleanp-of-system-validators-initp

(defthm booleanp-of-system-validators-initp
  (b* ((yes/no (system-validators-initp systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: system-validators-initp-of-system-state-fix-systate

(defthm system-validators-initp-of-system-state-fix-systate
  (equal (system-validators-initp (system-state-fix systate))
         (system-validators-initp systate)))

Theorem: system-validators-initp-system-state-equiv-congruence-on-systate

(defthm
   system-validators-initp-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (system-validators-initp systate)
                  (system-validators-initp systate-equiv)))
  :rule-classes :congruence)