		Search-engine friendly clone of the ACL2 documentation.

Create-nth-choice-count-alist

Make-nth-choice-list

Returns a list of the nth-preference candidates of all the voters

Signature
(make-nth-choice-list n xs) → choice-lst
Arguments: n — Guard (natp n).; xs — Guard (irv-ballot-p xs).
Returns: choice-lst — Type (nat-listp choice-lst), given the guard.

Definitions and Theorems

Theorem: natp-nth-of-nat-listp

(defthm natp-nth-of-nat-listp
  (implies (and (nat-listp lst)
                (< n (len lst))
                (natp n))
           (natp (nth n lst)))
  :rule-classes (:rewrite :type-prescription))

Theorem: member-of-nat-listp

(defthm member-of-nat-listp
  (implies (and (member-equal e lst)
                (nat-listp lst))
           (natp e)))

Function: make-nth-choice-list

(defun make-nth-choice-list (n xs)
  (declare (xargs :guard (and (natp n) (irv-ballot-p xs))))
  (let ((__function__ 'make-nth-choice-list))
    (declare (ignorable __function__))
    (if (endp xs)
        nil
      (if (< n (len (car xs)))
          (cons (nth n (car xs))
                (make-nth-choice-list n (cdr xs)))
        (make-nth-choice-list n (cdr xs))))))

Theorem: nat-listp-of-make-nth-choice-list

(defthm nat-listp-of-make-nth-choice-list
  (implies (and (natp n) (irv-ballot-p xs))
           (b* ((choice-lst (make-nth-choice-list n xs)))
             (nat-listp choice-lst)))
  :rule-classes :rewrite)

Theorem: make-nth-choice-list-of-xs=nil

(defthm make-nth-choice-list-of-xs=nil
  (equal (make-nth-choice-list n nil)
         nil))

Theorem: consp-of-0th-choice-occurrence-list

(defthm consp-of-0th-choice-occurrence-list
  (implies (and (consp xs) (irv-ballot-p xs))
           (consp (make-nth-choice-list 0 xs)))
  :rule-classes :type-prescription)

Theorem: len-of-0th-choice-occurrence-list

(defthm len-of-0th-choice-occurrence-list
  (implies (irv-ballot-p xs)
           (equal (len (make-nth-choice-list 0 xs))
                  (number-of-voters xs))))

Theorem: 0th-choice-occurrence-list-is-a-subset-of-all-candidates

(defthm 0th-choice-occurrence-list-is-a-subset-of-all-candidates
  (subsetp-equal (make-nth-choice-list 0 xs)
                 (candidate-ids xs)))

Theorem: make-nth-choice-list-returns-subset-of-all-cids

(defthm make-nth-choice-list-returns-subset-of-all-cids
  (implies (and (irv-ballot-p xs) (natp n))
           (subsetp-equal (make-nth-choice-list n xs)
                          (candidate-ids xs))))