Number of faulty validators in the system.
(number-faulty systate) → number
This is sometimes denoted
Function:
(defun number-faulty (systate) (declare (xargs :guard (system-statep systate))) (let ((__function__ 'number-faulty)) (declare (ignorable __function__)) (cardinality (faulty-addresses systate))))
Theorem:
(defthm natp-of-number-faulty (b* ((number (number-faulty systate))) (natp number)) :rule-classes :rewrite)
Theorem:
(defthm number-faulty-alt-def (equal (number-faulty systate) (- (number-validators systate) (number-correct systate))))
Theorem:
(defthm number-faulty-of-system-state-fix-systate (equal (number-faulty (system-state-fix systate)) (number-faulty systate)))
Theorem:
(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)