		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).

This is a synonym of the fixtype deconstructor, but it provides a bit of abstract, especially facilitating the extension of the model with stake, in which a committee will be not just a set of addresses.

Definitions and Theorems

Function: committee-members

(defun committee-members (commtt)
  (declare (xargs :guard (committeep commtt)))
  (let ((__function__ 'committee-members))
    (declare (ignorable __function__))
    (committee->addresses 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: not-emptyp-of-committee-members

(defthm not-emptyp-of-committee-members
  (b* ((?addresses (committee-members commtt)))
    (not (emptyp addresses))))

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)