		Search-engine friendly clone of the ACL2 documentation.

Committee

Committee->addresses

Get the addresses field from a committee.

Signature
(committee->addresses x) → addresses
Arguments: x — Guard (committeep x).
Returns: addresses — Type (address-setp addresses).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: committee->addresses$inline

(defun committee->addresses$inline (x)
  (declare (xargs :guard (committeep x)))
  (declare (xargs :guard t))
  (let ((__function__ 'committee->addresses))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x))
              (addresses (address-set-fix (cdr (std::da-nth 0 x)))))
           (if (emptyp addresses)
               (insert (address nil) nil)
             addresses))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: address-setp-of-committee->addresses

(defthm address-setp-of-committee->addresses
  (b* ((addresses (committee->addresses$inline x)))
    (address-setp addresses))
  :rule-classes :rewrite)

Theorem: committee->addresses$inline-of-committee-fix-x

(defthm committee->addresses$inline-of-committee-fix-x
  (equal (committee->addresses$inline (committee-fix x))
         (committee->addresses$inline x)))

Theorem: committee->addresses$inline-committee-equiv-congruence-on-x

(defthm committee->addresses$inline-committee-equiv-congruence-on-x
  (implies (committee-equiv x x-equiv)
           (equal (committee->addresses$inline x)
                  (committee->addresses$inline x-equiv)))
  :rule-classes :congruence)