		Search-engine friendly clone of the ACL2 documentation.

System-states

All-addresses

Set of the addresses of all the validators in the system.

Signature
(all-addresses systate) → addrs
Arguments: systate — Guard (system-statep systate).
Returns: addrs — Type (address-setp addrs).

These are the keys in the map.

Definitions and Theorems

Function: all-addresses

(defun all-addresses (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'all-addresses))
    (declare (ignorable __function__))
    (omap::keys (system-state->validators systate))))

Theorem: address-setp-of-all-addresses

(defthm address-setp-of-all-addresses
  (b* ((addrs (all-addresses systate)))
    (address-setp addrs))
  :rule-classes :rewrite)

Theorem: all-addresses-of-system-state-fix-systate

(defthm all-addresses-of-system-state-fix-systate
  (equal (all-addresses (system-state-fix systate))
         (all-addresses systate)))

Theorem: all-addresses-system-state-equiv-congruence-on-systate

(defthm all-addresses-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (all-addresses systate)
                  (all-addresses systate-equiv)))
  :rule-classes :congruence)