		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))))
  (or (emptyp x)
      (and (in (head x) y)
           (subset (left x) y)
           (subset (right x) y))))