(non-maj-ind-hint l cids xs) → (mv * * *)
Theorem:
(defthm candidate-with-least-nth-place-votes-is-a-member-of-cids-alt (implies (and (nat-listp cids) (consp cids) (irv-ballot-p xs)) (member-equal (candidate-with-least-nth-place-votes n cids xs) cids)))
Function:
(defun non-maj-ind-hint (l cids xs) (declare (xargs :guard t)) (let ((__function__ 'non-maj-ind-hint)) (declare (ignorable __function__)) (if (or (not (irv-ballot-p xs)) (endp cids) (endp xs)) (mv l cids xs) (b* ((step-2-candidate-to-remove (candidate-with-least-nth-place-votes 0 (candidate-ids xs) xs)) (new-xs (eliminate-candidate step-2-candidate-to-remove xs))) (if (equal l step-2-candidate-to-remove) (mv step-2-candidate-to-remove cids xs) (non-maj-ind-hint l (remove-equal step-2-candidate-to-remove cids) new-xs))))))