`member`

of one list is a `member`

of the other
Major Section: ACL2-BUILT-INS

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`

.

`Subsetp`

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