		Search-engine friendly clone of the ACL2 documentation.

Transitions-advance

Advance-possiblep

Check if a round advancement event is possible.

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

The val parameter of this function is the corresponding component of the advance event.

The validator must be a correct one. This is the only condition, since our round advancement logic is so simple.

Definitions and Theorems

Function: advance-possiblep

(defun advance-possiblep (val systate)
  (declare (xargs :guard (and (addressp val)
                              (system-statep systate))))
  (let ((__function__ 'advance-possiblep))
    (declare (ignorable __function__))
    (in (address-fix val)
        (correct-addresses systate))))

Theorem: booleanp-of-advance-possiblep

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

Theorem: advance-possiblep-of-address-fix-val

(defthm advance-possiblep-of-address-fix-val
  (equal (advance-possiblep (address-fix val)
                            systate)
         (advance-possiblep val systate)))

Theorem: advance-possiblep-address-equiv-congruence-on-val

(defthm advance-possiblep-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (advance-possiblep val systate)
                  (advance-possiblep val-equiv systate)))
  :rule-classes :congruence)

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

(defthm advance-possiblep-of-system-state-fix-systate
  (equal (advance-possiblep val (system-state-fix systate))
         (advance-possiblep val systate)))

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

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