• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/lists
• Remove

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)