		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Irv-ballot-p

Recognizer for a well-formed IRV ballot

Signature
(irv-ballot-p xs) → *

Definitions and Theorems

Function: irv-ballot-p

(defun irv-ballot-p (xs)
       (declare (xargs :guard t))
       (let ((__function__ 'irv-ballot-p))
            (declare (ignorable __function__))
            (if (consp xs)
                (b* ((one (car xs)) (rest (cdr xs)))
                    (and (nat-listp one)
                         one (no-duplicatesp-equal one)
                         (irv-ballot-p rest)))
                (equal xs nil))))

Theorem: irv-ballot-p-implies-non-empty-true-list-listp

(defthm irv-ballot-p-implies-non-empty-true-list-listp
        (implies (irv-ballot-p xs)
                 (non-empty-true-list-listp xs))
        :rule-classes :forward-chaining)

Theorem: irv-ballot-p-cdr

(defthm irv-ballot-p-cdr
        (implies (irv-ballot-p xs)
                 (irv-ballot-p (cdr xs))))

Subtopics

Non-empty-true-list-listp: Similar to true-list-listp, except that if x is non-empty, each element of x must be non-nil.