		Search-engine friendly clone of the ACL2 documentation.

Std/alists/remove-assoc-equal

Theorems about remove-assoc-equal in the std/alists library.

Theorem: alistp-of-remove-assoc-equal

(defthm alistp-of-remove-assoc-equal
  (implies (alistp x)
           (alistp (remove-assoc-equal a x))))

Theorem: acl2-count-of-remove-assoc-equal-upper-bound

(defthm acl2-count-of-remove-assoc-equal-upper-bound
  (<= (acl2-count (remove-assoc-equal a x))
      (acl2-count x))
  :rule-classes :linear)

Theorem: symbol-alistp-of-remove-assoc-equal

(defthm symbol-alistp-of-remove-assoc-equal
  (implies (symbol-alistp x)
           (symbol-alistp (remove-assoc-equal a x))))

Theorem: eqlable-alistp-of-remove-assoc-equal

(defthm eqlable-alistp-of-remove-assoc-equal
  (implies (eqlable-alistp x)
           (eqlable-alistp (remove-assoc-equal a x))))

Theorem: strip-cars-of-remove-assoc-equal

(defthm strip-cars-of-remove-assoc-equal
  (equal (strip-cars (remove-assoc-equal a x))
         (remove-equal a (strip-cars x))))