		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

All-head-to-head-competition-loser-p

Check if l will lose in a head-to-head competition against every candidate in cids

Signature
(all-head-to-head-competition-loser-p l cids xs) → *
Arguments: l — Possible loser.
Guard (natp l).; cids — All candidates in xs, except l.
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).

Definitions and Theorems

Function: all-head-to-head-competition-loser-p

(defun
 all-head-to-head-competition-loser-p
 (l cids xs)
 (declare (xargs :guard (and (natp l)
                             (nat-listp cids)
                             (irv-ballot-p xs))))
 (declare
      (xargs :guard (and (member-equal l (candidate-ids xs))
                         (not (member-equal l cids))
                         (subsetp-equal cids (candidate-ids xs)))))
 (let ((__function__ 'all-head-to-head-competition-loser-p))
      (declare (ignorable __function__))
      (if (endp cids)
          t
          (if (member-equal l cids)
              nil
              (if (head-to-head-competition-loser-p l (car cids)
                                                    xs)
                  (all-head-to-head-competition-loser-p l (cdr cids)
                                                        xs)
                  nil)))))

Subtopics

Head-to-head-competition-loser-p: Check if l will lose in a head-to-head competition against c