		Search-engine friendly clone of the ACL2 documentation.

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

Head-to-head-competition-loser-p

Check if l will lose in a head-to-head competition against c

Signature
(head-to-head-competition-loser-p l c xs) → *
Arguments: l — Possible loser.
Guard (natp l).; c — The other candidate in xs.
Guard (natp c).; xs — Guard (irv-ballot-p xs).

Definitions and Theorems

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

(defun head-to-head-competition-loser-p (l c xs)
  (declare (xargs :guard (and (natp l)
                              (natp c)
                              (irv-ballot-p xs))))
  (declare (xargs :guard (and (member-equal l (candidate-ids xs))
                              (member-equal c (candidate-ids xs))
                              (not (equal l c)))))
  (let ((__function__ 'head-to-head-competition-loser-p))
    (declare (ignorable __function__))
    (b* ((xs-pairwise (eliminate-other-candidates (list l c)
                                                  xs)))
      (equal (irv xs-pairwise) c))))