		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

Eliminate-candidates

Remove cids from xs

Signature
(eliminate-candidates cids xs) → new-xs
Arguments: cids — Candidates to remove.
Guard (nat-listp cids).; xs — Guard (irv-ballot-p xs).
Returns: new-xs — Type (irv-ballot-p new-xs), given (irv-ballot-p xs).

Definitions and Theorems

Function: eliminate-candidates

(defun eliminate-candidates (cids xs)
  (declare (xargs :guard (and (nat-listp cids)
                              (irv-ballot-p xs))))
  (let ((__function__ 'eliminate-candidates))
    (declare (ignorable __function__))
    (if (endp cids)
        xs
      (b* ((new-xs (eliminate-candidate (car cids) xs)))
        (eliminate-candidates (cdr cids)
                              new-xs)))))

Theorem: irv-ballot-p-of-eliminate-candidates

(defthm irv-ballot-p-of-eliminate-candidates
  (implies (irv-ballot-p xs)
           (b* ((new-xs (eliminate-candidates cids xs)))
             (irv-ballot-p new-xs)))
  :rule-classes :rewrite)

Theorem: eliminate-candidates-returns-a-subset-of-candidates

(defthm eliminate-candidates-returns-a-subset-of-candidates
  (subsetp-equal (candidate-ids (eliminate-candidates cids xs))
                 (candidate-ids xs)))

Theorem: intersectp-equal-and-remove-equal

(defthm intersectp-equal-and-remove-equal
  (implies (intersectp-equal x (remove-equal e y))
           (intersectp-equal x y)))

Theorem: eliminate-candidates-removes-no-candidate-when-cids-not-in-candidates

(defthm
 eliminate-candidates-removes-no-candidate-when-cids-not-in-candidates
 (implies (and (irv-ballot-p xs)
               (not (intersectp-equal cids (candidate-ids xs))))
          (equal (eliminate-candidates cids xs)
                 xs)))

Theorem: remove-equal-commutes

(defthm remove-equal-commutes
  (equal (remove-equal c1 (remove-equal c2 x))
         (remove-equal c2 (remove-equal c1 x))))

Theorem: eliminate-candidate-commutes

(defthm eliminate-candidate-commutes
  (equal (eliminate-candidate c1 (eliminate-candidate c2 xs))
         (eliminate-candidate c2 (eliminate-candidate c1 xs))))

Theorem: eliminate-candidates-and-eliminate-candidate-commute

(defthm eliminate-candidates-and-eliminate-candidate-commute
  (equal (eliminate-candidates cids (eliminate-candidate cid xs))
         (eliminate-candidate cid (eliminate-candidates cids xs))))

Theorem: eliminate-candidates-does-remove-candidates

(defthm eliminate-candidates-does-remove-candidates
 (implies
  (member-equal cid cids)
  (equal
       (member-equal cid
                     (candidate-ids (eliminate-candidates cids xs)))
       nil)))

Theorem: eliminate-candidates-removes-only-the-requested-candidates

(defthm eliminate-candidates-removes-only-the-requested-candidates
 (implies
  (not (member-equal c cids))
  (iff (member-equal c
                     (candidate-ids (eliminate-candidates cids xs)))
       (member-equal c (candidate-ids xs)))))

Theorem: candidate-ids-of-eliminate-candidates

(defthm candidate-ids-of-eliminate-candidates
  (equal (candidate-ids (eliminate-candidates cids xs))
         (remove-all cids (candidate-ids xs))))

Theorem: eliminate-candidates-where-cids=nil-does-not-modify-xs

(defthm eliminate-candidates-where-cids=nil-does-not-modify-xs
  (equal (eliminate-candidates nil xs)
         xs))