		Search-engine friendly clone of the ACL2 documentation.

Transitions

Events-next

New state resulting from a sequence of events.

Signature
(events-next events systate) → new-systate
Arguments: events — Guard (event-listp events).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

The sequence of events must be possible, as expressed by events-possiblep in the guard. If the sequence is empty, we return the input state. Otherwise, we execute the events from left to right.

Definitions and Theorems

Function: events-next

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

Theorem: system-statep-of-events-next

(defthm system-statep-of-events-next
  (b* ((new-systate (events-next events systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: correct-addresses-of-events-next

(defthm correct-addresses-of-events-next
  (implies (events-possiblep events systate)
           (b* ((?new-systate (events-next events systate)))
             (equal (correct-addresses new-systate)
                    (correct-addresses systate)))))