		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Undup-equiv

Signature
(undup-equiv x y) → *
Arguments: x — Guard (true-listp x).; y — Guard (true-listp y).

Definitions and Theorems

Function: undup-equiv

(defun undup-equiv (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (let ((__function__ 'undup-equiv))
    (declare (ignorable __function__))
    (equal (undup x) (undup y))))

Theorem: undup-equiv-is-an-equivalence

(defthm undup-equiv-is-an-equivalence
  (and (booleanp (undup-equiv x y))
       (undup-equiv x x)
       (implies (undup-equiv x y)
                (undup-equiv y x))
       (implies (and (undup-equiv x y)
                     (undup-equiv y z))
                (undup-equiv x z)))
  :rule-classes (:equivalence))

Theorem: undup-under-undup-equiv

(defthm undup-under-undup-equiv
  (undup-equiv (undup x) x))

Theorem: append-of-undup-under-undup-equiv-1

(defthm append-of-undup-under-undup-equiv-1
  (undup-equiv (append (undup x) y)
               (append x y)))

Theorem: append-of-undup-under-undup-equiv-2

(defthm append-of-undup-under-undup-equiv-2
  (undup-equiv (append x (undup y))
               (append x y)))

Theorem: undup-equiv-refines-set-equiv

(defthm undup-equiv-refines-set-equiv
  (implies (undup-equiv x y)
           (set-equiv x y))
  :rule-classes (:refinement))

Theorem: undup-equiv-implies-undup-equiv-append-1

(defthm undup-equiv-implies-undup-equiv-append-1
  (implies (undup-equiv a a-equiv)
           (undup-equiv (append a b)
                        (append a-equiv b)))
  :rule-classes (:congruence))

Theorem: undup-equiv-implies-undup-equiv-append-2

(defthm undup-equiv-implies-undup-equiv-append-2
  (implies (undup-equiv b b-equiv)
           (undup-equiv (append a b)
                        (append a b-equiv)))
  :rule-classes (:congruence))

Theorem: undup-equiv-implies-equal-undup-1

(defthm undup-equiv-implies-equal-undup-1
  (implies (undup-equiv x x-equiv)
           (equal (undup x) (undup x-equiv)))
  :rule-classes (:congruence))

Theorem: undup-equiv-of-list-fix-x

(defthm undup-equiv-of-list-fix-x
  (equal (undup-equiv (list-fix x) y)
         (undup-equiv x y)))

Theorem: undup-equiv-list-equiv-congruence-on-x

(defthm undup-equiv-list-equiv-congruence-on-x
  (implies (list-equiv x x-equiv)
           (equal (undup-equiv x y)
                  (undup-equiv x-equiv y)))
  :rule-classes :congruence)

Theorem: undup-equiv-of-list-fix-y

(defthm undup-equiv-of-list-fix-y
  (equal (undup-equiv x (list-fix y))
         (undup-equiv x y)))

Theorem: undup-equiv-list-equiv-congruence-on-y

(defthm undup-equiv-list-equiv-congruence-on-y
  (implies (list-equiv y y-equiv)
           (equal (undup-equiv x y)
                  (undup-equiv x y-equiv)))
  :rule-classes :congruence)