remove-assoc-equal

(in-package "ACL2")

(defsection std/alists/remove-assoc-equal
  :parents (std/alists remove-assoc)
  :short "Theorems about @(tsee remove-assoc-equal)
          in the @(see std/alists) library."
  (defthm alistp-of-remove-assoc-equal
    (implies (alistp x) (alistp (remove-assoc-equal a x))))
  (defthm acl2-count-of-remove-assoc-equal-upper-bound
    (<= (acl2-count (remove-assoc-equal a x)) (acl2-count x))
    :rule-classes :linear)
  (defthm symbol-alistp-of-remove-assoc-equal
    (implies (symbol-alistp x)
      (symbol-alistp (remove-assoc-equal a x))))
  (defthm eqlable-alistp-of-remove-assoc-equal
    (implies (eqlable-alistp x)
      (eqlable-alistp (remove-assoc-equal a x))))
  (defthm strip-cars-of-remove-assoc-equal
    (equal (strip-cars (remove-assoc-equal a x))
      (remove-equal a (strip-cars x)))))