		Search-engine friendly clone of the ACL2 documentation.

Std/lists/remove-duplicates-equal

Lemmas about remove-duplicates-equal available in the std/lists library.

Definitions and Theorems

Theorem: remove-duplicates-equal-when-atom

(defthm remove-duplicates-equal-when-atom
  (implies (atom x)
           (equal (remove-duplicates-equal x)
                  nil)))

Theorem: remove-duplicates-equal-of-cons

(defthm remove-duplicates-equal-of-cons
  (equal (remove-duplicates-equal (cons a x))
         (if (member a x)
             (remove-duplicates-equal x)
           (cons a (remove-duplicates-equal x)))))

Theorem: consp-of-remove-duplicates-equal

(defthm consp-of-remove-duplicates-equal
  (equal (consp (remove-duplicates-equal x))
         (consp x)))

Theorem: len-of-remove-duplicates-equal

(defthm len-of-remove-duplicates-equal
  (<= (len (remove-duplicates-equal x))
      (len x))
  :rule-classes ((:rewrite) (:linear)))

Theorem: remove-duplicates-equal-of-list-fix

(defthm remove-duplicates-equal-of-list-fix
  (equal (remove-duplicates-equal (list-fix x))
         (remove-duplicates-equal x)))

Theorem: list-equiv-implies-equal-remove-duplicates-equal-1

(defthm list-equiv-implies-equal-remove-duplicates-equal-1
  (implies (list-equiv x x-equiv)
           (equal (remove-duplicates-equal x)
                  (remove-duplicates-equal x-equiv)))
  :rule-classes (:congruence))

Theorem: set-equiv-implies-set-equiv-remove-duplicates-equal-1

(defthm set-equiv-implies-set-equiv-remove-duplicates-equal-1
  (implies (set-equiv x x-equiv)
           (set-equiv (remove-duplicates-equal x)
                      (remove-duplicates-equal x-equiv)))
  :rule-classes (:congruence))

Theorem: no-duplicatesp-equal-of-remove-duplicates-equal

(defthm no-duplicatesp-equal-of-remove-duplicates-equal
  (no-duplicatesp-equal (remove-duplicates-equal x)))

Theorem: duplicity-in-of-remove-duplicates-equal

(defthm duplicity-in-of-remove-duplicates-equal
  (equal (duplicity a (remove-duplicates-equal x))
         (if (member a x) 1 0)))

Theorem: remove-duplicates-equal-of-remove

(defthm remove-duplicates-equal-of-remove
  (equal (remove-duplicates-equal (remove a x))
         (remove a (remove-duplicates-equal x))))