		Search-engine friendly clone of the ACL2 documentation.

Union

An n-ary set union.

Time complexity: O(n\log(m/n)) (for binary union, where n < m).

Definitions and Theorems

Function: binary-union

(defun binary-union (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (let ((__function__ 'binary-union))
    (declare (ignorable __function__))
    (tree-union (sfix x) (sfix y))))

Theorem: setp-of-binary-union

(defthm setp-of-binary-union
  (b* ((set (binary-union x y)))
    (setp set))
  :rule-classes :rewrite)

Function: union-macro-loop

(defun union-macro-loop (list)
  (declare (xargs :guard (true-listp list)))
  (declare (xargs :guard (and (consp list) (consp (rest list)))))
  (let ((__function__ 'union-macro-loop))
    (declare (ignorable __function__))
    (if (endp (rest (rest list)))
        (list 'binary-union
              (first list)
              (second list))
      (list 'binary-union
            (first list)
            (union-macro-loop (rest list))))))