		Search-engine friendly clone of the ACL2 documentation.

Duplicity-badguy

Duplicity-badguy1

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

Definitions and Theorems

Function: duplicity-badguy1

(defun duplicity-badguy1 (dom x)
  (declare (xargs :guard t))
  (if (consp dom)
      (if (> (duplicity (car dom) x) 1)
          (list (car dom))
        (duplicity-badguy1 (cdr dom) x))
    nil))

Theorem: duplicity-badguy1-exists-in-list

(defthm duplicity-badguy1-exists-in-list
  (implies (duplicity-badguy1 dom x)
           (member-equal (car (duplicity-badguy1 dom x))
                         x)))

Theorem: duplicity-badguy1-exists-in-dom

(defthm duplicity-badguy1-exists-in-dom
  (implies (duplicity-badguy1 dom x)
           (member-equal (car (duplicity-badguy1 dom x))
                         dom)))

Theorem: duplicity-badguy1-has-high-duplicity

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

Theorem: duplicity-badguy1-is-complete-for-domain

(defthm duplicity-badguy1-is-complete-for-domain
  (implies (and (member-equal a dom)
                (< 1 (duplicity a x)))
           (duplicity-badguy1 dom x)))

Theorem: duplicity-badguy1-need-only-consider-the-list

(defthm duplicity-badguy1-need-only-consider-the-list
  (implies (duplicity-badguy1 dom x)
           (duplicity-badguy1 x x)))

Theorem: no-duplicatesp-equal-when-duplicity-badguy1

(defthm no-duplicatesp-equal-when-duplicity-badguy1
  (implies (and (not (duplicity-badguy1 dom x))
                (subsetp-equal x dom))
           (no-duplicatesp-equal x)))