- Practice writing equation-based programs
- Use engineering analysis to deal with numerical approximations
- Practice specifying correctness properties
- Use DrACuLa DoubleCheck for predicate-based, random testing
- Coach the ACL2 mechanical logic to verify software properties

- Define the following functions
- Package the functions you define as a book.
- DoubleCheck the properties stated below
- Use ACL2 to prove the properties
- Package the theorems as a book.

- Define a function insert-everywhere that, given a value x and a list xs, delivers a list xss whose elements are all like xs, but with x inserted among the elements. The list xss must contain one more element than xs, and for each index k, there must be a list in xss whose element of index k is x. (That is, the list xss must contain versions of xs with x in all possible positions.) The order of the lists in xss is is immaterial. For example, the value of (insert-everywhere 1 '(2 3)) could be ((1 2 3) (2 1 3) (2 3 1)), or it could be ((2 3 1) (2 1 3) (1 2 3)), or it could be other arrangements of the lists (1 2 3), (2 1 3), and (2 3 1).
- Define a function that delivers the list of permutations of a given list. The order in which the list arranges the permutations is immaterial. For example, either the list ((1 2 3) (1 3 2) (2 1 3) (2 3 1) (3 1 2) (3 2 1)) or the list ((1 2 3) (2 1 3) (2 3 1) (1 3 2) (3 1 2) (3 2 1)) or any of many other arrangements would be suitable values for (permutations '(1 2 3)).
- Define a function that finds an optimal route in the Euclidean bottleneck traveling
salesman problem (as described in Wikipedia).

*Note 1*: Include your max-min and permutations books in the code, and refer to their functions where you find them useful.

*Note 2*: Since the bottleneck version of the problem seeks only minimize the longest segment in a route (not the length of the whole route), you can use squared Euclidean distance as a proxy for Euclidean distance. This is fortunate, since Euclidean distance is usually not a rational number.

- State and prove a theorem about the relationship of the length of (insert-everywhere x xs) compared to the length of xs.
- State and prove a theorem that says that x is an element of every list in
(insert-everywhere x xs) [
*Hint*: Define a predicate (member-all x xss) whose value is non-nil if and only if the formula (member-equal x xs) is non-nil for every element xs of xss.] - State and prove a theorem that says that every list in (insert-everywhere
x xs) is a permutation of the list (cons x xs). [
*Hint*: See the the definition of perm, defined in Section 10.3 of the*Computer-Aided Reasoning*textbook] - Define a theorem that says that (permutations xs) is a true-list of true-lists, as long as xs is a true-list.