		Search-engine friendly clone of the ACL2 documentation.

Subset

Check if one set is a subset of the other.

Signature
(subset x y) → *
Arguments: x — Guard (setp x).; y — Guard (setp y).

Time complexity: O(n\log(m)) (Note: the current implementation is inefficient. This should eventually be O(n\log(m/n)), where n < m. This may be implemented similar to diff.)

Definitions and Theorems

Function: subset

(defun subset (x y)
  (declare (xargs :guard (and (setp x) (setp y))))
  (declare (xargs :type-prescription (booleanp (subset x y))))
  (let ((__function__ 'subset))
    (declare (ignorable __function__))
    (or (emptyp x)
        (and (in (head x) y)
             (subset (left x) y)
             (subset (right x) y)))))