Matt Kaufmann, 8/28/02 At the seminar today I intend to give a relatively short presentation on a tool that we expect to be useful at AMD, which I plan to make generally available since others might find it useful too. The tool implements the following spec from Rob Sumners. Input is a certifiable book, and output is two certifiable books: one that defines simpler functions corresponding to some of the input book's functions, and one that proves equivalence between the original and simplified definitions. (I'll say a few words about why such a tool might be useful.) I've made up a little example and run the tool on it, and I'll go through the example today as a way of explaining the tool. There are some cute ACL2 proof techniques, independent of the tool, that I'll point out.