		Search-engine friendly clone of the ACL2 documentation.

Transitions

Event-possiblep

Check if an event is possible.

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

Based on the event, we use the appropriate predicate.

Definitions and Theorems

Function: event-possiblep

(defun event-possiblep (event systate)
 (declare (xargs :guard (and (eventp event)
                             (system-statep systate))))
 (let ((__function__ 'event-possiblep))
  (declare (ignorable __function__))
  (event-case
    event
    :create-certificate
    (create-certificate-possiblep event.certificate systate)
    :receive-certificate
    (receive-certificate-possiblep event.message systate)
    :store-certificate
    (store-certificate-possiblep event.validator
                                 event.certificate systate)
    :advance-round (advance-round-possiblep event.validator systate)
    :commit-anchors
    (commit-anchors-possiblep event.validator systate)
    :timer-expires
    (timer-expires-possiblep event.validator systate))))

Theorem: booleanp-of-event-possiblep

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

Theorem: event-possiblep-of-event-fix-event

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

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

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

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

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

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

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