• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
      • Fairness-criteria
        • Eliminate-candidates
        • Sum-nats
        • Eliminate-other-candidates
        • Clone-p
        • Last-place
        • All-head-to-head-competition-loser-p
        • Non-maj-ind-hint
        • Find-condorcet-loser
        • Last-place-elim-ind-hint
      • Candidate-with-least-nth-place-votes
      • Eliminate-candidate
      • First-choice-of-majority-p
      • Candidate-ids
      • Irv
      • Create-nth-choice-count-alist
      • Irv-alt
      • Irv-ballot-p
      • Majority
      • Number-of-candidates
      • List-elements-equal
      • Number-of-voters
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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))