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).
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)