		Search-engine friendly clone of the ACL2 documentation.

Intersect

An n-ary set intersection.

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

Definitions and Theorems

Function: binary-intersect

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

Theorem: setp-of-binary-intersect

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

Function: intersect-macro-loop

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

Macro: intersect

(defmacro intersect (x y &rest rst)
  (declare (xargs :guard t))
  (intersect-macro-loop (list* x y rst)))