		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Number-of-voters

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

Definitions and Theorems

Function: number-of-voters

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

Theorem: natp-of-number-of-voters

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