		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.