		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

Non-maj-ind-hint

Signature
(non-maj-ind-hint l cids xs) → (mv * * *)

Definitions and Theorems

Theorem: candidate-with-least-nth-place-votes-is-a-member-of-cids-alt

(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: non-maj-ind-hint

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