`(union x y)` constructs the union of

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

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

**Function: **

(defun union (x y) (declare (xargs :guard (and (setp x) (setp y)))) (mbe :logic (if (empty x) (sfix y) (insert (head x) (union (tail x) y))) :exec (fast-union x y nil)))

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

(defthm union-empty-x (implies (empty x) (equal (union x y) (sfix y))))

**Theorem: **

(defthm union-empty-y (implies (empty y) (equal (union x y) (sfix x))))

**Theorem: **

(defthm union-empty (equal (empty (union x y)) (and (empty x) (empty y))))

**Theorem: **

(defthm union-in (equal (in a (union x y)) (or (in a x) (in a y))))

**Theorem: **

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

**Theorem: **

(defthm union-subset-x (subset x (union x y)))

**Theorem: **

(defthm union-subset-y (subset y (union x y)))

**Theorem: **

(defthm union-insert-x (equal (union (insert a x) y) (insert a (union x y))))

**Theorem: **

(defthm union-insert-y (equal (union x (insert a y)) (insert a (union x y))))

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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

**Theorem: **

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