		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