Major Section: PROGRAMMING
(Set-difference-equal x y) equals a list whose members
(see member-equal) contains the members of x that are not
members of y. More precisely, the resulting list is the same as
one gets by deleting the members of y from x, leaving the
remaining elements in the same order as they had in x.
The guard for set-difference-equal requires both arguments to be
true lists. Essentially, set-difference-equal has the same
functionality as the Common Lisp function set-difference, except
that it uses the equal function to test membership rather than
eql. However, we do not include the function set-difference
in ACL2, because the Common Lisp language does not specify the order
of the elements in the list that it returns.
Also see set-difference-eq for a semantically equivalent function that
executes more efficiently on lists of symbols.