		Search-engine friendly clone of the ACL2 documentation.

Committees

Committee-members

Addresses of the members of the committee.

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

The members of a committees are the keys of the map.

Definitions and Theorems

Function: committee-members

(defun committee-members (commtt)
  (declare (xargs :guard (committeep commtt)))
  (let ((__function__ 'committee-members))
    (declare (ignorable __function__))
    (omap::keys (committee->members-with-stake commtt))))

Theorem: address-setp-of-committee-members

(defthm address-setp-of-committee-members
  (b* ((addresses (committee-members commtt)))
    (address-setp addresses))
  :rule-classes :rewrite)

Theorem: committee-members-of-committee-fix-commtt

(defthm committee-members-of-committee-fix-commtt
  (equal (committee-members (committee-fix commtt))
         (committee-members commtt)))

Theorem: committee-members-committee-equiv-congruence-on-commtt

(defthm committee-members-committee-equiv-congruence-on-commtt
  (implies (committee-equiv commtt commtt-equiv)
           (equal (committee-members commtt)
                  (committee-members commtt-equiv)))
  :rule-classes :congruence)