`(intersect x y)` constructs the intersection of

The logical definition is very simple, and the essential
correctness property is given by

The execution uses a better, O(n) algorithm to intersect the sets by exploiting the set order.

See also intersectp, which doesn't construct a new set but just tells you whether the sets have any overlap. It's potentially faster if you don't care about constructing the set, because it doesn't have to do any consing.

**Function: **

(defun intersect (x y) (declare (xargs :guard (and (setp x) (setp y)))) (mbe :logic (cond ((empty x) (sfix x)) ((in (head x) y) (insert (head x) (intersect (tail x) y))) (t (intersect (tail x) y))) :exec (fast-intersect x y nil)))

**Theorem: **

(defthm intersect-set (setp (intersect x y)))

**Theorem: **

(defthm intersect-sfix-cancel-x (equal (intersect (sfix x) y) (intersect x y)))

**Theorem: **

(defthm intersect-sfix-cancel-y (equal (intersect x (sfix y)) (intersect x y)))

**Theorem: **

(defthm intersect-empty-x (implies (empty x) (empty (intersect x y))))

**Theorem: **

(defthm intersect-empty-y (implies (empty y) (empty (intersect x y))))

**Theorem: **

(defthm intersect-in (equal (in a (intersect x y)) (and (in a y) (in a x))))

**Theorem: **

(defthm intersect-symmetric (equal (intersect x y) (intersect y x)) :rule-classes ((:rewrite :loop-stopper ((x y)))))

**Theorem: **

(defthm intersect-subset-x (subset (intersect x y) x))

**Theorem: **

(defthm intersect-subset-y (subset (intersect x y) y))

**Theorem: **

(defthm intersect-insert-x (implies (not (in a y)) (equal (intersect (insert a x) y) (intersect x y))))

**Theorem: **

(defthm intersect-insert-y (implies (not (in a x)) (equal (intersect x (insert a y)) (intersect x y))))

**Theorem: **

(defthm intersect-with-subset-left (implies (subset x y) (equal (intersect x y) (sfix x))) :rule-classes ((:rewrite :backchain-limit-lst 1)))

**Theorem: **

(defthm intersect-with-subset-right (implies (subset x y) (equal (intersect y x) (sfix x))) :rule-classes ((:rewrite :backchain-limit-lst 1)))

**Theorem: **

(defthm intersect-self (equal (intersect x x) (sfix x)))

**Theorem: **

(defthm intersect-associative (equal (intersect (intersect x y) z) (intersect x (intersect y z))))

**Theorem: **

(defthm intersect-commutative (equal (intersect x (intersect y z)) (intersect y (intersect x z))) :rule-classes ((:rewrite :loop-stopper ((x y)))))

**Theorem: **

(defthm intersect-outer-cancel (equal (intersect x (intersect x z)) (intersect x z)))