		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Create-nth-choice-count-alist

Create a count-alistp for nth-preference candidates

Signature
(create-nth-choice-count-alist n cids xs) → count-alst
Arguments: n — Guard (natp n).; cids — All the candidates in the election, sorted.
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).
Returns: count-alst — Type (alistp count-alst).

Definitions and Theorems

Function: create-nth-choice-count-alist

(defun create-nth-choice-count-alist
       (n cids xs)
       (declare (xargs :guard (and (natp n)
                                   (nat-listp cids)
                                   (irv-ballot-p xs))))
       (let ((__function__ 'create-nth-choice-count-alist))
            (declare (ignorable __function__))
            (b* ((choice-lst (make-nth-choice-list n xs))
                 (count-alst (create-count-alist cids choice-lst)))
                count-alst)))

Theorem: alistp-of-create-nth-choice-count-alist

(defthm alistp-of-create-nth-choice-count-alist
        (b* ((count-alst (create-nth-choice-count-alist n cids xs)))
            (alistp count-alst))
        :rule-classes :rewrite)

Theorem: count-alistp-of-create-nth-choice-count-alist

(defthm
     count-alistp-of-create-nth-choice-count-alist
     (b* ((?count-alst (create-nth-choice-count-alist n cids xs)))
         (implies (nat-listp cids)
                  (count-alistp count-alst))))

Theorem: strip-cars-of-create-nth-choice-count-alist-is-sorted-if-cids-is-sorted

(defthm
 strip-cars-of-create-nth-choice-count-alist-is-sorted-if-cids-is-sorted
 (b* ((?count-alst (create-nth-choice-count-alist n cids xs)))
     (implies (acl2::<-ordered-p cids)
              (acl2::<-ordered-p (strip-cars count-alst)))))

Theorem: consp-of-create-nth-choice-count-alist

(defthm consp-of-create-nth-choice-count-alist
        (equal (consp (create-nth-choice-count-alist n cids xs))
               (consp cids)))

Theorem: strip-cars-of-create-nth-choice-count-alist-equal-under-set-equiv

(defthm
   strip-cars-of-create-nth-choice-count-alist-equal-under-set-equiv
   (b* ((?count-alst (create-nth-choice-count-alist n cids xs)))
       (acl2::set-equiv (strip-cars count-alst)
                        cids)))

Theorem: no-duplicatesp-equal-of-strip-cars-of-create-nth-choice-count-alist

(defthm
 no-duplicatesp-equal-of-strip-cars-of-create-nth-choice-count-alist
 (implies
      (no-duplicatesp-equal cids)
      (no-duplicatesp-equal
           (strip-cars (create-nth-choice-count-alist n cids xs)))))

Theorem: member-of-strip-cars-of-create-nth-choice-count-alist

(defthm
 member-of-strip-cars-of-create-nth-choice-count-alist
 (implies
      (member-equal id cids)
      (member-equal
           id
           (strip-cars (create-nth-choice-count-alist n cids xs)))))

Theorem: member-of-strip-cdrs-of-create-nth-choice-count-alist

(defthm member-of-strip-cdrs-of-create-nth-choice-count-alist
        (b* ((count-alst (create-nth-choice-count-alist n cids xs)))
            (implies (member-equal id cids)
                     (member-equal (cdr (assoc-equal id count-alst))
                                   (strip-cdrs count-alst)))))

Theorem: len-of-create-nth-choice-count-alist-0th-choice

(defthm len-of-create-nth-choice-count-alist-0th-choice
        (equal (len (create-nth-choice-count-alist 0 cids xs))
               (len cids)))

Subtopics

Create-count-alist: Given a choice list, maps each candidate ID to the number of votes they obtained
Make-nth-choice-list: Returns a list of the nth-preference candidates of all the voters