`(delete a x)` removes the element

If

Efficiency note. Delete is

The theorem

**Function: **

(defun delete (a x) (declare (xargs :guard (setp x))) (mbe :logic (cond ((empty x) nil) ((equal a (head x)) (tail x)) (t (insert (head x) (delete a (tail x))))) :exec (cond ((endp x) nil) ((equal a (car x)) (cdr x)) (t (insert (car x) (delete a (cdr x)))))))

**Theorem: **

(defthm delete-set (setp (delete a x)))

**Theorem: **

(defthm delete-preserves-empty (implies (empty x) (empty (delete a x))))

**Theorem: **

(defthm delete-in (equal (in a (delete b x)) (and (in a x) (not (equal a b)))))

**Theorem: **

(defthm delete-sfix-cancel (equal (delete a (sfix x)) (delete a x)))

**Theorem: **

(defthm delete-nonmember-cancel (implies (not (in a x)) (equal (delete a x) (sfix x))))

**Theorem: **

(defthm delete-delete (equal (delete a (delete b x)) (delete b (delete a x))) :rule-classes ((:rewrite :loop-stopper ((a b)))))

**Theorem: **

(defthm repeated-delete (equal (delete a (delete a x)) (delete a x)))

**Theorem: **

(defthm delete-insert-cancel (equal (delete a (insert a x)) (delete a x)))

**Theorem: **

(defthm insert-delete-cancel (equal (insert a (delete a x)) (insert a x)))

**Theorem: **

(defthm subset-delete (subset (delete a x) x))