		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Irv-alt

An alternative (but equivalent) definition of irv, with the majority step removed

Signature
(irv-alt xs) → *
Arguments: xs — Guard (irv-ballot-p xs).

The following theorem says that irv-alt and irv can be used interchangeably.

Theorem: irv-alt-equiv-to-irv

(defthm irv-alt-equiv-to-irv
  (equal (irv-alt xs) (irv xs)))

Definitions and Theorems

Function: irv-alt

(defun irv-alt (xs)
 (declare (xargs :guard (irv-ballot-p xs)))
 (let ((__function__ 'irv-alt))
  (declare (ignorable __function__))
  (if
   (mbt (irv-ballot-p xs))
   (if (endp xs)
       nil
     (b*
      ((cids (candidate-ids xs))
       ((if (equal (len cids) 1)) (car cids))
       (step-2-candidate-to-remove
            (candidate-with-least-nth-place-votes 0 cids xs))
       (new-xs (eliminate-candidate step-2-candidate-to-remove xs)))
      (irv-alt new-xs)))
   nil)))

Theorem: min-nats-is-<=-than-any-other-list-element

(defthm min-nats-is-<=-than-any-other-list-element
  (implies (and (member-equal e x) (nat-listp x))
           (<= (min-nats x) e))
  :rule-classes :linear)

Theorem: max-nats-is->=-than-any-other-list-element

(defthm max-nats-is->=-than-any-other-list-element
  (implies (and (member-equal e x) (nat-listp x))
           (<= e (max-nats x)))
  :rule-classes :linear)

Theorem: first-choice-of-majority-p-cannot-be-candidates-with-min-votes

(defthm
     first-choice-of-majority-p-cannot-be-candidates-with-min-votes
 (implies
  (and (equal m
              (first-choice-of-majority-p (candidate-ids xs)
                                          xs))
       (< 1 (number-of-candidates xs))
       (irv-ballot-p xs))
  (not (member-equal
            m
            (candidates-with-min-votes
                 (create-nth-choice-count-alist 0 (candidate-ids xs)
                                                xs))))))

Theorem: candidate-with-least-nth-place-votes-member-of-candidates-with-min-votes-0th-place

(defthm
 candidate-with-least-nth-place-votes-member-of-candidates-with-min-votes-0th-place
 (implies
     (and (< 1 (number-of-candidates xs))
          (irv-ballot-p xs))
     (member-equal
          (candidate-with-least-nth-place-votes 0 (candidate-ids xs)
                                                xs)
          (candidates-with-min-votes
               (create-nth-choice-count-alist 0 (candidate-ids xs)
                                              xs)))))

Theorem: first-choice-of-majority-p-and-candidate-with-least-nth-place-votes-are-different

(defthm
 first-choice-of-majority-p-and-candidate-with-least-nth-place-votes-are-different
 (implies
  (and (< 1 (number-of-candidates xs))
       (irv-ballot-p xs))
  (not
   (equal (first-choice-of-majority-p (candidate-ids xs)
                                      xs)
          (candidate-with-least-nth-place-votes 0 (candidate-ids xs)
                                                xs)))))

Theorem: irv-alt-equiv-to-irv

(defthm irv-alt-equiv-to-irv
  (equal (irv-alt xs) (irv xs)))