Returns a list of the
(make-nth-choice-list n xs) → choice-lst
Theorem:
(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:
(defthm member-of-nat-listp (implies (and (member-equal e lst) (nat-listp lst)) (natp e)))
Function:
(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:
(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:
(defthm make-nth-choice-list-of-xs=nil (equal (make-nth-choice-list n nil) nil))
Theorem:
(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:
(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:
(defthm 0th-choice-occurrence-list-is-a-subset-of-all-candidates (subsetp-equal (make-nth-choice-list 0 xs) (candidate-ids xs)))
Theorem:
(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))))