		Search-engine friendly clone of the ACL2 documentation.

System-states

Number-correct

Number of correct validators in the system.

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

Definitions and Theorems

Function: number-correct

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

Theorem: natp-of-number-correct

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

Theorem: number-correct-upper-bound

(defthm number-correct-upper-bound
  (b* ((common-lisp::?number (number-correct systate)))
    (<= number (number-validators systate)))
  :rule-classes :linear)

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

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

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

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