		Search-engine friendly clone of the ACL2 documentation.

Instant-runoff-voting

List-elements-equal

Returns t if all elements of x are equal to e

Signature
(list-elements-equal e x) → elem-equal?
Arguments: x — Guard (true-listp x).
Returns: elem-equal? — Type (booleanp elem-equal?).

Definitions and Theorems

Function: list-elements-equal

(defun list-elements-equal (e x)
       (declare (xargs :guard (true-listp x)))
       (let ((__function__ 'list-elements-equal))
            (declare (ignorable __function__))
            (if (endp x)
                t
                (and (equal (car x) e)
                     (list-elements-equal e (cdr x))))))

Theorem: booleanp-of-list-elements-equal

(defthm booleanp-of-list-elements-equal
        (b* ((elem-equal? (list-elements-equal e x)))
            (booleanp elem-equal?))
        :rule-classes :type-prescription)