Reading our answers doesn't help you! Nevertheless, if you've really given up, you can find the answers here (in the form of an ACL2 input file) and you can see ACL2's output in response to our answers here.
We also include the Latex source, in order to make it easy to quote from this
paper. We hereby give permission to quote freely from this paper, provided
none of the quoted text is modified and full attribution is given.
main.tex (100 KB Latex source)
main.bib (6 KB bibtex bibliographic database)
llncs.cls (35 KB LNCS file defining documentclass llncs)
acl2.sty (1 KB ACL2 Latex package)
Finally, here are solutions to the exercises and the corresponding prover
output. If you are learning to use ACL2, try to avoid the temptation to look
at the solutions until after you have attempted the exercises yourself.
(24 KB exercise solutions)
(200 KB exercise solutions output)