		Search-engine friendly clone of the ACL2 documentation.

Moddb.lisp

Wirelist-remove-name

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

Definitions and Theorems

Function: wirelist-remove-name

(defun wirelist-remove-name (name x)
  (declare (xargs :guard (and (name-p name) (wirelist-p x))))
  (let ((__function__ 'wirelist-remove-name))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (if (mbe :logic (name-equiv (wire->name (car x)) name)
               :exec (equal (wire->name (car x)) name))
          (wirelist-remove-name name (cdr x))
        (cons (wire-fix (car x))
              (wirelist-remove-name name (cdr x)))))))

Theorem: wirelist-p-of-wirelist-remove-name

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

Theorem: wirelist-remove-name-of-name-fix-name

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

Theorem: wirelist-remove-name-name-equiv-congruence-on-name

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

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

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

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

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

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

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

Theorem: wirelist-remove-name-when-not-member

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