		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

Majority

Signature
(majority n) → maj
Arguments: n — Number of voters.
Guard (natp n).
Returns: maj — Type (natp maj), given the guard.

Definitions and Theorems

Function: majority

(defun majority (n)
  (declare (xargs :guard (natp n)))
  (let ((__function__ 'majority))
    (declare (ignorable __function__))
    (if (evenp n) (/ n 2) (/ (- n 1) 2))))

Theorem: natp-of-majority

(defthm natp-of-majority
  (implies (and (natp n))
           (b* ((maj (majority n))) (natp maj)))
  :rule-classes :type-prescription)

Theorem: majority-is-less-than-total

(defthm majority-is-less-than-total
  (implies (posp n) (< (majority n) n))
  :rule-classes :linear)

Theorem: majority-may-increase-if-num-voters-increase

(defthm majority-may-increase-if-num-voters-increase
  (implies (and (< m n) (natp m) (natp n))
           (<= (majority m) (majority n)))
  :rule-classes :linear)

Theorem: majority-upper-bound

(defthm majority-upper-bound
  (and (implies (posp x) (< (majority x) x))
       (implies (natp x) (<= (majority x) x)))
  :rule-classes :linear)