(split n xs) -- delivers (list prefix suffix) where prefix is
the first n elements of xs and suffix is the remaining elements
Example: (split 3 (list 1 2 3 4 5 6 7)) is (list (list 1 2 3) (list 4 5 6
7))
The following intrinsic ACL2 functions will be useful in this problem
- (length xs)
- (true-listp xs)
Notes:
- You probably will need to look at some details of ACL2 proof attempts and apply The Method
- You may find it useful to put use-instance hints in some theorems.