		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

Eliminate-other-candidates

Remove all candidates from xs, except for those in cids

Signature
(eliminate-other-candidates cids xs) → new-xs
Arguments: cids — Candidates to preserve.
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

Theorem: nat-listp-of-set-difference-equal

(defthm nat-listp-of-set-difference-equal
  (implies (nat-listp x)
           (nat-listp (set-difference-equal x y))))

Function: eliminate-other-candidates

(defun eliminate-other-candidates (cids xs)
 (declare (xargs :guard (and (nat-listp cids)
                             (irv-ballot-p xs))))
 (let ((__function__ 'eliminate-other-candidates))
   (declare (ignorable __function__))
   (b* ((candidates-to-remove (remove-all cids (candidate-ids xs))))
     (eliminate-candidates candidates-to-remove xs))))

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

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

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

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

Theorem: cids-is-a-subset-of-eliminate-other-candidates

(defthm cids-is-a-subset-of-eliminate-other-candidates
  (implies
       (subsetp-equal cids (candidate-ids xs))
       (subsetp-equal
            cids
            (candidate-ids (eliminate-other-candidates cids xs)))))

Theorem: eliminate-other-candidates-equal-to-cids-under-set-equiv

(defthm eliminate-other-candidates-equal-to-cids-under-set-equiv
  (implies (subsetp-equal cids (candidate-ids xs))
           (acl2::set-equiv
                (candidate-ids (eliminate-other-candidates cids xs))
                cids)))

Theorem: eliminate-other-candidates-does-not-modify-xs-when-cids=candidate-ids

(defthm
 eliminate-other-candidates-does-not-modify-xs-when-cids=candidate-ids
 (implies (acl2::set-equiv cids (candidate-ids xs))
          (equal (eliminate-other-candidates cids xs)
                 xs)))

Subtopics

Remove-all: Remove all elements in x from y