SET-DIFFERENCE-EQUAL

elements of one list that are not elements of another
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.