		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

Last-place

Index of the last-place vote in xs

Signature
(last-place xs) → lp
Arguments: xs — Guard (irv-ballot-p xs).
Returns: lp — Type (natp lp).

Definitions and Theorems

Theorem: posp-number-of-candidates

(defthm posp-number-of-candidates
  (implies (and (irv-ballot-p xs) (consp xs))
           (posp (number-of-candidates xs))))

Function: last-place

(defun last-place (xs)
  (declare (xargs :guard (irv-ballot-p xs)))
  (let ((__function__ 'last-place))
    (declare (ignorable __function__))
    (if (and (irv-ballot-p xs) (consp xs))
        (1- (number-of-candidates xs))
      0)))

Theorem: natp-of-last-place

(defthm natp-of-last-place
  (b* ((lp (last-place xs))) (natp lp))
  :rule-classes :type-prescription)

Theorem: last-place-after-eliminate-candidate

(defthm last-place-after-eliminate-candidate
  (implies (and (irv-ballot-p xs)
                (< 1 (number-of-candidates xs)))
           (equal (last-place (eliminate-candidate id xs))
                  (if (member-equal id (candidate-ids xs))
                      (1- (last-place xs))
                    (last-place xs)))))

Theorem: last-place-of-cdr-xs

(defthm last-place-of-cdr-xs
  (implies (irv-ballot-p xs)
           (<= (last-place (cdr xs))
               (last-place xs)))
  :rule-classes (:linear :rewrite))