		Search-engine friendly clone of the ACL2 documentation.

Std/lists/remove

Lemmas about remove available in the std/lists library.

Definitions and Theorems

Theorem: remove-when-atom

(defthm remove-when-atom
  (implies (atom x)
           (equal (remove a x) nil)))

Theorem: remove-of-cons

(defthm remove-of-cons
  (equal (remove a (cons b x))
         (if (equal a b)
             (remove a x)
           (cons b (remove a x)))))

Theorem: consp-of-remove

(defthm consp-of-remove
  (equal (consp (remove a x))
         (not (subsetp x (list a)))))

Theorem: remove-under-iff

(defthm remove-under-iff
  (iff (remove a x)
       (not (subsetp x (list a)))))

Theorem: remove-when-non-member

(defthm remove-when-non-member
  (implies (not (member a x))
           (equal (remove a x) (list-fix x))))

Theorem: upper-bound-of-len-of-remove-weak

(defthm upper-bound-of-len-of-remove-weak
  (<= (len (remove a x)) (len x))
  :rule-classes ((:rewrite) (:linear)))

Theorem: upper-bound-of-len-of-remove-strong

(defthm upper-bound-of-len-of-remove-strong
  (implies (member a x)
           (< (len (remove a x)) (len x)))
  :rule-classes :linear)

Theorem: len-of-remove-exact

(defthm len-of-remove-exact
  (equal (len (remove a x))
         (- (len x) (duplicity a x))))

Theorem: remove-is-commutative

(defthm remove-is-commutative
  (equal (remove b (remove a x))
         (remove a (remove b x))))

Theorem: remove-is-idempotent

(defthm remove-is-idempotent
  (equal (remove a (remove a x))
         (remove a x)))

Theorem: duplicity-of-remove

(defthm duplicity-of-remove
  (equal (duplicity a (remove b x))
         (if (equal a b) 0 (duplicity a x))))

Theorem: remove-of-append

(defthm remove-of-append
  (equal (remove a (append x y))
         (append (remove a x) (remove a y))))

Theorem: remove-of-revappend

(defthm remove-of-revappend
  (equal (remove a (revappend x y))
         (revappend (remove a x) (remove a y))))

Theorem: remove-of-rev

(defthm remove-of-rev
  (equal (remove a (rev x))
         (rev (remove a x))))

Theorem: remove-of-union-equal

(defthm remove-of-union-equal
  (equal (remove a (union-equal x y))
         (union-equal (remove a x)
                      (remove a y))))

Theorem: remove-of-intersection-equal

(defthm remove-of-intersection-equal
  (equal (remove a (intersection-equal x y))
         (intersection-equal (remove a x)
                             (remove a y))))

Theorem: remove-of-set-difference-equal

(defthm remove-of-set-difference-equal
  (equal (remove a (set-difference-equal x y))
         (set-difference-equal (remove a x) y)))

Theorem: element-list-p-of-remove

(defthm element-list-p-of-remove
  (implies (element-list-p x)
           (element-list-p (remove a x)))
  :rule-classes :rewrite)