• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Acre
    • Milawa
    • Smtlink
    • Aleobft
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
      • Fairness-criteria
        • Eliminate-candidates
        • Sum-nats
        • Eliminate-other-candidates
          • Remove-all
        • Clone-p
        • Last-place
        • All-head-to-head-competition-loser-p
        • Non-maj-ind-hint
        • Find-condorcet-loser
        • Last-place-elim-ind-hint
      • Candidate-with-least-nth-place-votes
      • Eliminate-candidate
      • First-choice-of-majority-p
      • Candidate-ids
      • Irv
      • Create-nth-choice-count-alist
      • Irv-alt
      • Irv-ballot-p
      • Majority
      • Number-of-candidates
      • List-elements-equal
      • Number-of-voters
    • Imp-language
    • Sidekick
    • Leftist-trees
    • C
    • Java
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Riscv
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Bigmems
    • Builtins
    • Axe
    • Execloader
    • Solidity
    • Leo
    • Paco
    • Concurrent-programs
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Eliminate-other-candidates

Remove-all

Remove all elements in x from y

Signature

(remove-all x y) → *

Arguments

x — Guard (true-listp x).

y — Guard (true-listp y).

Definitions and Theorems

Function: remove-all

(defun remove-all (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))))
  (let ((__function__ 'remove-all))
    (declare (ignorable __function__))
    (if (endp x)
        y
      (remove-all (cdr x)
                  (remove-equal (car x) y)))))

Theorem: remove-all-cons-to-remove-all-remove-equal

(defthm remove-all-cons-to-remove-all-remove-equal
  (equal (remove-all (cons e x) y)
         (remove-all x (remove-equal e y))))

Theorem: remove-all-x-and-cdr-x

(defthm remove-all-x-and-cdr-x
  (equal (remove-all x (cdr x)) nil))

Theorem: remove-all-x-x-is-nil

(defthm remove-all-x-x-is-nil
  (implies (true-listp x)
           (equal (remove-all x x) nil)))

Theorem: remove-all-and-remove-equal-commute

(defthm remove-all-and-remove-equal-commute
  (equal (remove-all as (remove-equal e bs))
         (remove-equal e (remove-all as bs))))

Theorem: remove-all-commutes

(defthm remove-all-commutes
  (equal (remove-all as (remove-all bs cs))
         (remove-all bs (remove-all as cs))))

Theorem: remove-all-returns-a-subset-of-the-list

(defthm remove-all-returns-a-subset-of-the-list
  (subsetp-equal (remove-all x y) y))

Theorem: remove-all-and-member-equal-1

(defthm remove-all-and-member-equal-1
  (implies (member-equal e a)
           (equal (member-equal e (remove-all a b))
                  nil)))

Theorem: remove-all-and-member-equal-2

(defthm remove-all-and-member-equal-2
  (implies (not (member-equal e a))
           (iff (member-equal e (remove-all a b))
                (member-equal e b))))

Theorem: remove-all-of-nil-is-nil

(defthm remove-all-of-nil-is-nil
  (equal (remove-all x nil) nil))

Theorem: remove-all-x-from-cons-e-y

(defthm remove-all-x-from-cons-e-y
  (equal (remove-all x (cons e y))
         (if (member-equal e x)
             (remove-all x y)
           (cons e (remove-all x y)))))

Theorem: remove-all-superset-from-subset-is-nil

(defthm remove-all-superset-from-subset-is-nil
  (implies (and (subsetp-equal y x) (true-listp y))
           (equal (remove-all x y) nil)))

Theorem: remove-all-and-set-equiv

(defthm remove-all-and-set-equiv
  (implies (and (acl2::set-equiv x y)
                (true-listp y))
           (equal (remove-all x y) nil)))

Theorem: nested-remove-alls-and-subsetp-equal

(defthm nested-remove-alls-and-subsetp-equal
  (implies (subsetp-equal a c)
           (subsetp-equal a (remove-all (remove-all a b) c))))