(concat xss) -- elements of the list xss (which are,
themselves, lists) concatenated, forming a single list
Example: (concat (list 1 2 3) (list 4 5 6 7) (list 8 9) is the list (1 2 3 4
5 6 7 8 9)
The following intrinsic ACL2 functions will be useful in this problem
- (length xs)
- (member-equal x xs)
- (true-list-listp xss)
To state the necessary predicates, it will be helpful to define the following functions
- (sum-of-lengths xss) -- the sum of the lengths of the lists in xss
- (member-some x xss) -- true if and only if x is an element of at least one of the lists in xss.