		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: all-addresses-of-events-next

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

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)))))

Theorem: faulty-addresses-of-events-next

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

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

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

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

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

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

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

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

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