		Search-engine friendly clone of the ACL2 documentation.

Committees

Committee-max-faulty

Maximum tolerated number of faulty validators in a committee.

Signature
(committee-max-faulty commtt) → maxf
Arguments: commtt — Guard (committeep commtt).
Returns: maxf — Type (natp maxf).

The f discussed in max-faulty-for-total applies to a committee, not to the whole system, in the same way as n.

Definitions and Theorems

Function: committee-max-faulty

(defun committee-max-faulty (commtt)
  (declare (xargs :guard (committeep commtt)))
  (let ((__function__ 'committee-max-faulty))
    (declare (ignorable __function__))
    (max-faulty-for-total (committee-total commtt))))

Theorem: natp-of-committee-max-faulty

(defthm natp-of-committee-max-faulty
  (b* ((maxf (committee-max-faulty commtt)))
    (natp maxf))
  :rule-classes (:rewrite :type-prescription))

Theorem: committee-max-faulty-of-committee-fix-commtt

(defthm committee-max-faulty-of-committee-fix-commtt
  (equal (committee-max-faulty (committee-fix commtt))
         (committee-max-faulty commtt)))

Theorem: committee-max-faulty-committee-equiv-congruence-on-commtt

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