		Search-engine friendly clone of the ACL2 documentation.

Std/lists/remove1-equal

Lemmas about remove1 available in the std/lists library.

Definitions and Theorems

Theorem: len-of-remove1-equal

(defthm len-of-remove1-equal
  (equal (len (remove1-equal x l))
         (if (member-equal x l)
             (- (len l) 1)
           (len l))))

Theorem: assoc-equal-of-remove1-equal

(defthm assoc-equal-of-remove1-equal
  (implies (and (not (equal key1 nil))
                (not (consp (assoc-equal key1 alist))))
           (not (consp (assoc-equal key1 (remove1-equal x alist)))))
  :rule-classes (:rewrite :type-prescription))

Theorem: member-equal-of-remove1-equal

(defthm member-equal-of-remove1-equal
  (implies (not (equal x1 x2))
           (iff (member-equal x1 (remove1-equal x2 l))
                (member-equal x1 l))))

Theorem: subsetp-equal-of-remove1-equal-left

(defthm subsetp-equal-of-remove1-equal-left
  (implies (subsetp-equal x y)
           (subsetp-equal (remove1-equal a x) y)))