UNION-EQUAL

Major Section:  PROGRAMMING

(Union-equal x y) equals a list whose members (see member-equal) contains the members of x and the members of y. More precisely, the resulting list is the same as one would get by first deleting the members of y from x, and then concatenating the result to the front of y.

The guard for union-equal requires both arguments to be true lists. Essentially, union-equal has the same functionality as the Common Lisp function union, except that it uses the equal function to test membership rather than eql. However, we do not include the function union in ACL2, because the Common Lisp language does not specify the order of the elements in the list that it returns.