		Search-engine friendly clone of the ACL2 documentation.

Duplicity-badguy

(duplicity-badguy x) finds an element that occurs multiple times in the list x, if one exists.

This function is central to our proof of no-duplicatesp-equal-same-by-duplicity, a pick-a-point style strategy for proving that no-duplicatesp holds of a list by reasoning about duplicity of an arbitrary element.

Definitions and Theorems

Function: duplicity-badguy

(defun duplicity-badguy (x)
  (declare (xargs :guard t))
  (duplicity-badguy1 x x))

Theorem: duplicity-badguy-exists

(defthm duplicity-badguy-exists
  (implies (duplicity-badguy x)
           (member-equal (car (duplicity-badguy x))
                         x)))

Theorem: duplicity-badguy-has-high-duplicity

(defthm duplicity-badguy-has-high-duplicity
  (implies (duplicity-badguy x)
           (< 1
              (duplicity (car (duplicity-badguy x))
                         x))))

Theorem: duplicity-badguy-is-complete

(defthm duplicity-badguy-is-complete
  (implies (< 1 (duplicity a x))
           (duplicity-badguy x)))

Theorem: duplicity-badguy-under-iff

(defthm duplicity-badguy-under-iff
  (iff (duplicity-badguy x)
       (not (no-duplicatesp-equal x))))

Subtopics

Duplicity-badguy1: (duplicity-badguy1 dom x) finds the first element of dom whose duplicity in x exceeds 1, if such a member exists.