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