### Homework 5, Due 11/15/2002 (before midnight)

This will be a group project. Groups of size 2-4 are allowed.
Please form groups on your own (perhaps by using the newsgroup).
The goal of this homework is to familiarize you with proving
theorems using the theorem prover. Read chapters 8 and 9 of the
Computer-Aided Reasoning book. As is stated in the book, once you
know what to prove, the most difficulty part is determining what
lemmas are needed to guide the theorem prover. These lemmas tend
to be the same ones needed for hand proofs and since you already
thought about the lemmas needed for the problems in homework 4,
this assignment consists of doing homework 4 with ACL2 (instead
of by hand).

Create a file "homework5.lisp" that contains the definitions
and theorems you were asked to provide for homework 4. A skeleton file to get you started is available
here. To check that it works as
expected, check that your file contains all of the `defthm`s in
the skeleton file (you may wind up rearranging the order in which
theorems are proved), and in a fresh ACL2,
certify the book, *i.e.*, `(certify-book
"homework5")` should generate a certificate without any
errors (you will get warnings about not checking guards, etc.,
but should not get any errors).

Send the text file with your
answers via email to both Vernard (vernard@cc) and myself.