		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Wirelist-nodups-p

Signature
(wirelist-nodups-p x) → *

Definitions and Theorems

Function: wirelist-nodups-p

(defun wirelist-nodups-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'wirelist-nodups-p))
    (declare (ignorable __function__))
    (and (wirelist-p x)
         (no-duplicatesp-equal (wirelist->names x)))))

Theorem: wirelist-nodups-p-implies-wirelist-p

(defthm wirelist-nodups-p-implies-wirelist-p
  (implies (wirelist-nodups-p x)
           (wirelist-p x)))

Theorem: wirelist-nodups-p-of-append

(defthm wirelist-nodups-p-of-append
  (implies (and (wirelist-nodups-p a)
                (wirelist-nodups-p b)
                (not (intersection$ (wirelist->names a)
                                    (wirelist->names b))))
           (wirelist-nodups-p (append a b))))

Theorem: wirelist-nodups-p-of-cons

(defthm wirelist-nodups-p-of-cons
  (equal (wirelist-nodups-p (cons a b))
         (and (wire-p a)
              (wirelist-nodups-p b)
              (not (member (wire->name a)
                           (wirelist->names b))))))