		Search-engine friendly clone of the ACL2 documentation.

Subsetp

Test if every member of one list is a member of the other

General Forms:
(subsetp x y)
(subsetp x y :test 'eql)   ; same as above (eql as equality test)
(subsetp x y :test 'eq)    ; same, but eq is equality test
(subsetp x y :test 'equal) ; same, but equal is equality test

(Subsetp x y) is true if and only if every member of the list x is a member of the list y. The optional keyword, :TEST, has no effect logically, but provides the test (default eql) used for comparing members of the two lists.

The guard for a call of subsetp depends on the test. In all cases, both arguments must satisfy true-listp. If the test is eql, then one of the arguments must satisfy eqlable-listp. If the test is eq, then one of the arguments must satisfy symbol-listp.

See equality-variants for a discussion of the relation between subsetp and its variants:

(subsetp-eq x lst) is equivalent to (subsetp x lst :test 'eq);

(subsetp-equal x lst) is equivalent to (subsetp x lst :test 'equal).

In particular, reasoning about any of these primitives reduces to reasoning about the function subsetp-equal.

Function: subsetp-equal

(defun subsetp-equal (x y)
  (declare (xargs :guard (and (true-listp y) (true-listp x))))
  (cond ((endp x) t)
        ((member-equal (car x) y)
         (subsetp-equal (cdr x) y))
        (t nil)))

Subsetp is defined by Common Lisp. See any Common Lisp documentation for more information.

Subtopics

Std/lists/subsetp: Lemmas about subsetp available in the std/lists library.