		Search-engine friendly clone of the ACL2 documentation.

Reachability

System-state-reachablep

Check if a system state is reachable from some initial state.

Definitions and Theorems

Theorem: system-state-reachablep-suff

(defthm system-state-reachablep-suff
  (implies (and (system-statep from)
                (system-initp from)
                (system-state-reachable-from-p systate from))
           (system-state-reachablep systate)))

Theorem: booleanp-of-system-state-reachablep

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

Theorem: system-state-reachablep-of-system-state-fix-systate

(defthm system-state-reachablep-of-system-state-fix-systate
  (equal (system-state-reachablep (system-state-fix systate))
         (system-state-reachablep systate)))

Theorem: system-state-reachablep-system-state-equiv-congruence-on-systate

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