		Search-engine friendly clone of the ACL2 documentation.

Find-condorcet-loser

Find-condorcet-loser-aux

Signature
(find-condorcet-loser-aux loser-cids cids xs) → *
Arguments: loser-cids — Candidates in xs to consider as losers.
Guard (nat-listp loser-cids).; cids — All candidates in xs.
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).

Definitions and Theorems

Function: find-condorcet-loser-aux

(defun find-condorcet-loser-aux (loser-cids cids xs)
  (declare (xargs :guard (and (nat-listp loser-cids)
                              (nat-listp cids)
                              (irv-ballot-p xs))))
  (declare
       (xargs :guard (and (acl2::set-equiv cids (candidate-ids xs))
                          (subsetp-equal loser-cids cids))))
  (let ((__function__ 'find-condorcet-loser-aux))
    (declare (ignorable __function__))
    (if (endp loser-cids)
        nil
      (if (all-head-to-head-competition-loser-p
               (car loser-cids)
               (remove-equal (car loser-cids) cids)
               xs)
          (car loser-cids)
        (find-condorcet-loser-aux (cdr loser-cids)
                                  cids xs)))))