• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
        • Duplicity-badguy
          • Duplicity-badguy1
        • No-duplicatesp-equal-same-by-duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Std/lists/add-to-set
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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)))