		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Number-of-candidates

Signature
(number-of-candidates xs) → num
Arguments: xs — Guard (irv-ballot-p xs).
Returns: num — Type (natp num).

Definitions and Theorems

Function: number-of-candidates

(defun number-of-candidates (xs)
  (declare (xargs :guard (irv-ballot-p xs)))
  (let ((__function__ 'number-of-candidates))
    (declare (ignorable __function__))
    (len (candidate-ids xs))))

Theorem: natp-of-number-of-candidates

(defthm natp-of-number-of-candidates
  (b* ((num (number-of-candidates xs)))
    (natp num))
  :rule-classes :type-prescription)

Theorem: number-of-candidates-is-exactly-one-lemma

(defthm number-of-candidates-is-exactly-one-lemma
  (implies (and (irv-ballot-p xs)
                (consp xs)
                (<= (number-of-candidates xs) 1))
           (equal (number-of-candidates xs) 1)))