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