		Search-engine friendly clone of the ACL2 documentation.

Reachability

System-state-reachable-from-p

Check if a system state is reachable from another one.

This is the case when there is a list of zero or more events that are possible in the starting state (one after the other), and that lead to the state of interest (one after the other).

Definitions and Theorems

Theorem: system-state-reachable-from-p-suff

(defthm system-state-reachable-from-p-suff
  (implies (and (event-listp events)
                (events-possiblep events from)
                (equal (system-state-fix systate)
                       (events-next events from)))
           (system-state-reachable-from-p systate from)))

Theorem: booleanp-of-system-state-reachable-from-p

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

Theorem: system-state-reachable-from-p-of-system-state-fix-systate

(defthm system-state-reachable-from-p-of-system-state-fix-systate
  (equal (system-state-reachable-from-p (system-state-fix systate)
                                        from)
         (system-state-reachable-from-p systate from)))

Theorem: system-state-reachable-from-p-system-state-equiv-congruence-on-systate

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

Theorem: system-state-reachable-from-p-of-system-state-fix-from

(defthm system-state-reachable-from-p-of-system-state-fix-from
 (equal
     (system-state-reachable-from-p systate (system-state-fix from))
     (system-state-reachable-from-p systate from)))

Theorem: system-state-reachable-from-p-system-state-equiv-congruence-on-from

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