		Search-engine friendly clone of the ACL2 documentation.

Committee

Committee->members-with-stake

Get the members-with-stake field from a committee.

Signature
(committee->members-with-stake x) → members-with-stake
Arguments: x — Guard (committeep x).
Returns: members-with-stake — Type (address-pos-mapp members-with-stake).

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

Definitions and Theorems

Function: committee->members-with-stake$inline

(defun committee->members-with-stake$inline (x)
  (declare (xargs :guard (committeep x)))
  (declare (xargs :guard t))
  (let ((__function__ 'committee->members-with-stake))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (address-pos-map-fix (cdr (std::da-nth 0 x))))
         :exec (cdr (std::da-nth 0 x)))))

Theorem: address-pos-mapp-of-committee->members-with-stake

(defthm address-pos-mapp-of-committee->members-with-stake
 (b* ((members-with-stake (committee->members-with-stake$inline x)))
   (address-pos-mapp members-with-stake))
 :rule-classes :rewrite)

Theorem: committee->members-with-stake$inline-of-committee-fix-x

(defthm committee->members-with-stake$inline-of-committee-fix-x
  (equal (committee->members-with-stake$inline (committee-fix x))
         (committee->members-with-stake$inline x)))

Theorem: committee->members-with-stake$inline-committee-equiv-congruence-on-x

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