		Search-engine friendly clone of the ACL2 documentation.

Committees

Committee-total-stake

Total stake of validators in a committee.

Signature
(committee-total-stake commtt) → total
Arguments: commtt — Guard (committeep commtt).
Returns: total — Type (natp total).

This is n, using the notation in max-faulty-for-total. It is the sum of all the units of stake associated to members of the committee.

Definitions and Theorems

Function: committee-total-stake

(defun committee-total-stake (commtt)
  (declare (xargs :guard (committeep commtt)))
  (let ((__function__ 'committee-total-stake))
    (declare (ignorable __function__))
    (committee-members-stake (committee-members commtt)
                             commtt)))

Theorem: natp-of-committee-total-stake

(defthm natp-of-committee-total-stake
  (b* ((total (committee-total-stake commtt)))
    (natp total))
  :rule-classes (:rewrite :type-prescription))

Theorem: posp-of-committee-total-stake

(defthm posp-of-committee-total-stake
  (implies (committee-nonemptyp commtt)
           (b* ((total (committee-total-stake commtt)))
             (posp total)))
  :rule-classes (:rewrite :type-prescription))

Theorem: committee-total-stake-of-committee-fix-commtt

(defthm committee-total-stake-of-committee-fix-commtt
  (equal (committee-total-stake (committee-fix commtt))
         (committee-total-stake commtt)))

Theorem: committee-total-stake-committee-equiv-congruence-on-commtt

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