Returns a list of the

- 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.

**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))))