		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Wirelist-remove-names

Signature
(wirelist-remove-names names x) → xx
Arguments: names — Guard (namelist-p names).; x — Guard (wirelist-p x).
Returns: xx — Type (wirelist-p xx).

Definitions and Theorems

Function: wirelist-remove-names

(defun wirelist-remove-names (names x)
  (declare (xargs :guard (and (namelist-p names)
                              (wirelist-p x))))
  (let ((__function__ 'wirelist-remove-names))
    (declare (ignorable __function__))
    (if (atom names)
        (wirelist-fix x)
      (wirelist-remove-name (car names)
                            (wirelist-remove-names (cdr names)
                                                   x)))))

Theorem: wirelist-p-of-wirelist-remove-names

(defthm wirelist-p-of-wirelist-remove-names
  (b* ((xx (wirelist-remove-names names x)))
    (wirelist-p xx))
  :rule-classes :rewrite)

Theorem: wirelist-remove-names-of-nil

(defthm wirelist-remove-names-of-nil
  (equal (wirelist-remove-names nil x)
         (wirelist-fix x)))

Theorem: wirelist-remove-names-of-nil-second

(defthm wirelist-remove-names-of-nil-second
  (equal (wirelist-remove-names x nil)
         nil))

Theorem: wirelist-remove-names-of-cons-second

(defthm wirelist-remove-names-of-cons-second
  (equal (wirelist-remove-names x (cons y z))
         (if (member (wire->name y) (namelist-fix x))
             (wirelist-remove-names x z)
           (cons (wire-fix y)
                 (wirelist-remove-names x z)))))

Theorem: wirelist-remove-name-commute

(defthm wirelist-remove-name-commute
  (equal (wirelist-remove-name b (wirelist-remove-name a x))
         (wirelist-remove-name a (wirelist-remove-name b x)))
  :rule-classes ((:rewrite :loop-stopper ((b a)))))

Theorem: wirelist-remove-name-of-remove-names

(defthm wirelist-remove-name-of-remove-names
  (equal (wirelist-remove-name a (wirelist-remove-names names x))
         (wirelist-remove-names names (wirelist-remove-name a x))))

Theorem: wirelist-remove-name-of-remove-names-rev

(defthm wirelist-remove-name-of-remove-names-rev
  (equal (wirelist-remove-names names (wirelist-remove-name a x))
         (wirelist-remove-name a (wirelist-remove-names names x))))

Theorem: wirelist-remove-names-of-remove-name

(defthm wirelist-remove-names-of-remove-name
  (implies (not (member (name-fix name)
                        (wirelist->names x)))
           (equal (wirelist-remove-names (remove-equal name names)
                                         x)
                  (wirelist-remove-names names x))))

Theorem: wirelist-remove-names-of-remove-later-duplicates

(defthm wirelist-remove-names-of-remove-later-duplicates
 (equal (wirelist-remove-names (acl2::remove-later-duplicates names)
                               x)
        (wirelist-remove-names names x)))

Theorem: wirelist-remove-names-of-namelist-fix-names

(defthm wirelist-remove-names-of-namelist-fix-names
  (equal (wirelist-remove-names (namelist-fix names)
                                x)
         (wirelist-remove-names names x)))

Theorem: wirelist-remove-names-namelist-equiv-congruence-on-names

(defthm wirelist-remove-names-namelist-equiv-congruence-on-names
  (implies (namelist-equiv names names-equiv)
           (equal (wirelist-remove-names names x)
                  (wirelist-remove-names names-equiv x)))
  :rule-classes :congruence)

Theorem: wirelist-remove-names-of-wirelist-fix-x

(defthm wirelist-remove-names-of-wirelist-fix-x
  (equal (wirelist-remove-names names (wirelist-fix x))
         (wirelist-remove-names names x)))

Theorem: wirelist-remove-names-wirelist-equiv-congruence-on-x

(defthm wirelist-remove-names-wirelist-equiv-congruence-on-x
  (implies (wirelist-equiv x x-equiv)
           (equal (wirelist-remove-names names x)
                  (wirelist-remove-names names x-equiv)))
  :rule-classes :congruence)