		Search-engine friendly clone of the ACL2 documentation.

Fairness-criteria

Sum-nats

Signature
(sum-nats lst) → sum
Arguments: lst — Guard (nat-listp lst).
Returns: sum — Type (natp sum), given (nat-listp lst).

Definitions and Theorems

Function: sum-nats

(defun sum-nats (lst)
  (declare (xargs :guard (nat-listp lst)))
  (let ((__function__ 'sum-nats))
    (declare (ignorable __function__))
    (if (endp lst)
        0
      (+ (car lst) (sum-nats (cdr lst))))))

Theorem: natp-of-sum-nats

(defthm natp-of-sum-nats
  (implies (nat-listp lst)
           (b* ((sum (sum-nats lst))) (natp sum)))
  :rule-classes (:type-prescription :rewrite))

Theorem: sum-nats-lower-bound

(defthm sum-nats-lower-bound
  (implies (and (member-equal e lst)
                (nat-listp lst))
           (<= e (sum-nats lst)))
  :rule-classes :linear)

Theorem: majority-+-lemma

(defthm majority-+-lemma
  (implies (and (<= j (majority x))
                (natp i)
                (natp j)
                (natp x))
           (<= j (majority (+ i x))))
  :rule-classes (:linear :rewrite))

Theorem: majority-lower-bound-lemma

(defthm majority-lower-bound-lemma
  (implies (and (natp x) (natp j) (<= j x))
           (<= j (majority (+ j x)))))

Theorem: sum-nats->-majority-is-unique-1

(defthm sum-nats->-majority-is-unique-1
  (implies (and (< (majority (sum-nats x)) j)
                (member-equal j x)
                (member-equal i x)
                (nat-listp x)
                (natp j))
           (<= i j))
  :rule-classes nil)

Theorem: sum-nats-majority-duplicity=1

(defthm sum-nats-majority-duplicity=1
  (implies (and (< (majority (sum-nats lst)) e)
                (member-equal e lst)
                (nat-listp lst))
           (equal (acl2::duplicity e lst) 1)))

Theorem: sum-nats->-majority-is-unique-2

(defthm sum-nats->-majority-is-unique-2
  (implies (and (< (majority (sum-nats x)) j)
                (< (majority (sum-nats x)) i)
                (member-equal j x)
                (member-equal i x)
                (nat-listp x))
           (equal i j))
  :rule-classes nil)

Theorem: sum-nats-of-count-alist-of-empty-choice-list

(defthm sum-nats-of-count-alist-of-empty-choice-list
  (equal (sum-nats (strip-cdrs (create-count-alist cids nil)))
         0))

Theorem: sum-nats-cons-e-x=sum-nats-x-if-e=0

(defthm sum-nats-cons-e-x=sum-nats-x-if-e=0
  (implies (natp e)
           (iff (equal (sum-nats (cons e x))
                       (sum-nats x))
                (equal e 0))))

Theorem: sum-nats-of-strip-cdrs-of-create-count-alist-is-len-y

(defthm sum-nats-of-strip-cdrs-of-create-count-alist-is-len-y
  (implies (and (no-duplicatesp-equal x)
                (subsetp-equal y x))
           (equal (sum-nats (strip-cdrs (create-count-alist x y)))
                  (len y))))

Theorem: sum-nats-strip-cdrs-create-nth-choice-count-alist==number-of-voters

(defthm
 sum-nats-strip-cdrs-create-nth-choice-count-alist==number-of-voters
 (implies
  (and (irv-ballot-p xs)
       (no-duplicatesp-equal cids)
       (acl2::set-equiv cids (candidate-ids xs)))
  (equal
   (sum-nats (strip-cdrs (create-nth-choice-count-alist 0 cids xs)))
   (number-of-voters xs))))