### append

### Purpose of exercise

- Practice specifying correctness properties
- Use DrACuLa DoubleCheck for predicate-based, random testing
- Learn about importing books of theorems to support the theorem proving
process
- Certify correctness properties using ACL2

### Activities

- Package DoubleCheck tests for the properties stated below in a book (the "test book"), and run some tests
- Convert the DoubleCheck predicates to ACL2 theorems, package them in another book (the "verification book"), and certify it
- Here are some
predefined functions that you might find helpful

### Terminology

*true-list*: nil or (cons x xs), where xs is a true-list (the
predicate true-listp tests for true-lists)

### Properties

- The first (length xs) elements of (append xs ys) is xs
- (append xs ys) without its first (length xs) elements is ys
- The length of the list append delivers is the sum of the lengths of its
arguments
- Appending the first n elements of a list with its elements beyond the
first n reproduces the list

### ACL2 instrinsics and other functions useful in this exercise

- true-listp
- len
- natp
- NthCdr
- firstN

### Useful books of theorems