		Search-engine friendly clone of the ACL2 documentation.

Candidate-with-least-nth-place-votes

Candidates-with-min-votes

Returns a list of candidates, if any, which received the minimum number of votes

Signature
(candidates-with-min-votes count-alst) → cids
Arguments: count-alst — Guard (count-alistp count-alst).
Returns: cids — Type (nat-listp cids), given the guard.

Definitions and Theorems

Function: candidates-with-min-votes

(defun candidates-with-min-votes (count-alst)
  (declare (xargs :guard (count-alistp count-alst)))
  (let ((__function__ 'candidates-with-min-votes))
    (declare (ignorable __function__))
    (b* ((min-num-of-votes (min-nats (strip-cdrs count-alst))))
      (all-keys min-num-of-votes count-alst))))

Theorem: nat-listp-of-candidates-with-min-votes

(defthm nat-listp-of-candidates-with-min-votes
  (implies (and (count-alistp count-alst))
           (b* ((cids (candidates-with-min-votes count-alst)))
             (nat-listp cids)))
  :rule-classes :rewrite)

Theorem: natp-car-of-candidates-with-min-votes

(defthm natp-car-of-candidates-with-min-votes
  (b* ((?cids (candidates-with-min-votes count-alst)))
    (implies (and (count-alistp count-alst) cids)
             (natp (car cids))))
  :rule-classes (:rewrite :type-prescription))

Theorem: candidates-with-min-votes-is-non-empty

(defthm candidates-with-min-votes-is-non-empty
  (implies (and (count-alistp count-alst)
                (consp count-alst))
           (and (candidates-with-min-votes count-alst)
                (consp (candidates-with-min-votes count-alst)))))

Theorem: candidates-with-min-votes-returns-a-subset-of-candidates

(defthm candidates-with-min-votes-returns-a-subset-of-candidates
  (subsetp-equal (candidates-with-min-votes count-alst)
                 (strip-cars count-alst)))

Subtopics

All-keys: Returns a list of all the keys in alst with the value val
Min-nats: Pick the minimum number in a list of natural numbers