		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