		Search-engine friendly clone of the ACL2 documentation.

System-states

Number-faulty

Number of faulty validators in the system.

Signature
(number-faulty systate) → number
Arguments: systate — Guard (system-statep systate).
Returns: number — Type (natp number).

This is sometimes denoted f in the literature, but the same symbol sometimes instead denotes the maximum tolerated number of faulty validators. See the discussion in max-faulty-for-total.

Definitions and Theorems

Function: number-faulty

(defun number-faulty (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'number-faulty))
    (declare (ignorable __function__))
    (cardinality (faulty-addresses systate))))

Theorem: natp-of-number-faulty

(defthm natp-of-number-faulty
  (b* ((number (number-faulty systate)))
    (natp number))
  :rule-classes :rewrite)

Theorem: number-faulty-alt-def

(defthm number-faulty-alt-def
  (equal (number-faulty systate)
         (- (number-validators systate)
            (number-correct systate))))

Theorem: number-faulty-of-system-state-fix-systate

(defthm number-faulty-of-system-state-fix-systate
  (equal (number-faulty (system-state-fix systate))
         (number-faulty systate)))

Theorem: number-faulty-system-state-equiv-congruence-on-systate

(defthm number-faulty-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (number-faulty systate)
                  (number-faulty systate-equiv)))
  :rule-classes :congruence)