		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$inline

(defun binary-intersect$inline (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (tree-intersect (sfix x) (sfix y)))

Theorem: setp-of-binary-intersect

(defthm setp-of-binary-intersect
  (b* ((set (binary-intersect$inline 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)))))
  (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)))