		Search-engine friendly clone of the ACL2 documentation.

Transitions

Events-possiblep

Check if a sequence of events is possible.

Signature
(events-possiblep events systate) → yes/no
Arguments: events — Guard (event-listp events).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

Each event must be possible in the state that immediately precedes it, starting with the input systate for the first state in events (i.e. the car, because we consider these events left to right), and using event-next to calculate the state for each successive event. This predicate returns t on the empty list of events, since no events can always happen, so to speak.

Definitions and Theorems

Function: events-possiblep

(defun events-possiblep (events systate)
  (declare (xargs :guard (and (event-listp events)
                              (system-statep systate))))
  (let ((__function__ 'events-possiblep))
    (declare (ignorable __function__))
    (b* (((when (endp events)) t)
         ((unless (event-possiblep (car events) systate))
          nil))
      (events-possiblep (cdr events)
                        (event-next (car events) systate)))))

Theorem: booleanp-of-events-possiblep

(defthm booleanp-of-events-possiblep
  (b* ((yes/no (events-possiblep events systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: events-possiblep-of-event-list-fix-events

(defthm events-possiblep-of-event-list-fix-events
  (equal (events-possiblep (event-list-fix events)
                           systate)
         (events-possiblep events systate)))

Theorem: events-possiblep-event-list-equiv-congruence-on-events

(defthm events-possiblep-event-list-equiv-congruence-on-events
  (implies (event-list-equiv events events-equiv)
           (equal (events-possiblep events systate)
                  (events-possiblep events-equiv systate)))
  :rule-classes :congruence)

Theorem: events-possiblep-of-system-state-fix-systate

(defthm events-possiblep-of-system-state-fix-systate
  (equal (events-possiblep events (system-state-fix systate))
         (events-possiblep events systate)))

Theorem: events-possiblep-system-state-equiv-congruence-on-systate

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