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 defthms 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.