Lemmas about intersection$ available in the std/lists library.

We'll take intersectp as the desired normal form for asking whether intersections are empty.

**Theorem: **

(defthm intersection$-under-iff (iff (intersection$ x y) (intersectp x y)))

**Theorem: **

(defthm consp-of-intersection$ (equal (consp (intersection$ x y)) (intersectp x y)))

Basic atom/cons rules.

**Theorem: **

(defthm intersection$-when-atom-left (implies (atom x) (equal (intersection$ x y) nil)))

**Theorem: **

(defthm intersection$-of-cons-left (equal (intersection$ (cons a x) y) (if (member a y) (cons a (intersection$ x y)) (intersection$ x y))))

**Theorem: **

(defthm intersection$-when-atom-right (implies (atom y) (equal (intersection$ x y) nil)))

We don't have a very nice rule for cons on the right if we're
trying to maintain

**Theorem: **

(defthm intersection$-of-cons-right-under-set-equiv (set-equiv (intersection$ x (cons a y)) (if (member a x) (cons a (intersection$ x y)) (intersection$ x y))))

**Theorem: **

(defthm member-of-intersection$ (iff (member a (intersection$ x y)) (and (member a x) (member a y))) :rule-classes (:rewrite (:type-prescription :corollary (implies (not (member a x)) (not (member a (intersection$ x y))))) (:type-prescription :corollary (implies (not (member a y)) (not (member a (intersection$ x y)))))))

**Theorem: **

(defthm subsetp-equal-of-intersection$-1 (subsetp-equal (intersection$ x y) x))

**Theorem: **

(defthm subsetp-equal-of-intersection$-2 (subsetp-equal (intersection$ x y) y))

**Theorem: **

(defthm intersection$-commutes-under-set-equiv (set-equiv (intersection$ x y) (intersection$ y x)))

Here is a nice bounding theorem. Note that there is no analogous rule for

(intersection$ '(a a a) '(a)) ==> '(a a a)

**Theorem: **

(defthm len-of-intersection$-upper-bound (<= (len (intersection$ x y)) (len x)) :rule-classes ((:rewrite) (:linear)))