		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Wirelist-rem-dups

Signature
(wirelist-rem-dups x) → xx
Arguments: x — Guard (wirelist-p x).
Returns: xx — Type (wirelist-nodups-p xx).

Definitions and Theorems

Function: wirelist-rem-dups

(defun wirelist-rem-dups (x)
  (declare (xargs :guard (wirelist-p x)))
  (let ((__function__ 'wirelist-rem-dups))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (cons (wire-fix (car x))
            (wirelist-remove-name (wire->name (car x))
                                  (wirelist-rem-dups (cdr x)))))))

Theorem: wirelist-nodups-p-of-wirelist-rem-dups

(defthm wirelist-nodups-p-of-wirelist-rem-dups
  (b* ((xx (wirelist-rem-dups x)))
    (wirelist-nodups-p xx))
  :rule-classes :rewrite)

Theorem: wirelist->names-of-remove-duplicate-names

(defthm wirelist->names-of-remove-duplicate-names
  (equal (wirelist->names (wirelist-rem-dups x))
         (acl2::remove-later-duplicates (wirelist->names x))))

Theorem: wirelist-rem-dups-when-no-duplicates

(defthm wirelist-rem-dups-when-no-duplicates
  (implies (no-duplicatesp (wirelist->names x))
           (equal (wirelist-rem-dups x)
                  (wirelist-fix x))))

Theorem: wirelist-rem-dups-when-wirelist-nodups-p

(defthm wirelist-rem-dups-when-wirelist-nodups-p
  (implies (wirelist-nodups-p x)
           (equal (wirelist-rem-dups x) x)))

Theorem: no-duplicate-names-of-wirelist-rem-dups

(defthm no-duplicate-names-of-wirelist-rem-dups
  (no-duplicatesp (wirelist->names (wirelist-rem-dups x))))

Theorem: wirelist-rem-dups-of-wirelist-fix-x

(defthm wirelist-rem-dups-of-wirelist-fix-x
  (equal (wirelist-rem-dups (wirelist-fix x))
         (wirelist-rem-dups x)))

Theorem: wirelist-rem-dups-wirelist-equiv-congruence-on-x

(defthm wirelist-rem-dups-wirelist-equiv-congruence-on-x
  (implies (wirelist-equiv x x-equiv)
           (equal (wirelist-rem-dups x)
                  (wirelist-rem-dups x-equiv)))
  :rule-classes :congruence)

Function: wirelist-nodups-equiv$inline

(defun wirelist-nodups-equiv$inline (x y)
  (declare (xargs :guard (and (wirelist-nodups-p x)
                              (wirelist-nodups-p y))))
  (equal (wirelist-rem-dups x)
         (wirelist-rem-dups y)))

Theorem: wirelist-nodups-equiv-is-an-equivalence

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

Theorem: wirelist-nodups-equiv-implies-equal-wirelist-rem-dups-1

(defthm wirelist-nodups-equiv-implies-equal-wirelist-rem-dups-1
  (implies (wirelist-nodups-equiv x x-equiv)
           (equal (wirelist-rem-dups x)
                  (wirelist-rem-dups x-equiv)))
  :rule-classes (:congruence))

Theorem: wirelist-rem-dups-under-wirelist-nodups-equiv

(defthm wirelist-rem-dups-under-wirelist-nodups-equiv
  (wirelist-nodups-equiv (wirelist-rem-dups x)
                         x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-wirelist-rem-dups-1-forward-to-wirelist-nodups-equiv

(defthm
      equal-of-wirelist-rem-dups-1-forward-to-wirelist-nodups-equiv
  (implies (equal (wirelist-rem-dups x) y)
           (wirelist-nodups-equiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-wirelist-rem-dups-2-forward-to-wirelist-nodups-equiv

(defthm
      equal-of-wirelist-rem-dups-2-forward-to-wirelist-nodups-equiv
  (implies (equal x (wirelist-rem-dups y))
           (wirelist-nodups-equiv x y))
  :rule-classes :forward-chaining)

Theorem: wirelist-nodups-equiv-of-wirelist-rem-dups-1-forward

(defthm wirelist-nodups-equiv-of-wirelist-rem-dups-1-forward
  (implies (wirelist-nodups-equiv (wirelist-rem-dups x)
                                  y)
           (wirelist-nodups-equiv x y))
  :rule-classes :forward-chaining)

Theorem: wirelist-nodups-equiv-of-wirelist-rem-dups-2-forward

(defthm wirelist-nodups-equiv-of-wirelist-rem-dups-2-forward
  (implies (wirelist-nodups-equiv x (wirelist-rem-dups y))
           (wirelist-nodups-equiv x y))
  :rule-classes :forward-chaining)

Theorem: wirelist-rem-dups-of-append

(defthm wirelist-rem-dups-of-append
  (equal (wirelist-rem-dups (append a b))
         (append (wirelist-rem-dups a)
                 (wirelist-remove-names (wirelist->names a)
                                        (wirelist-rem-dups b)))))