		Search-engine friendly clone of the ACL2 documentation.

Std/alists/remove-assoc-equal

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

Definitions and Theorems

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))))