Homework Assignment 1
                               CS 389r

                        Unique Numbers: 52120
                             Spring, 2015

                       Given:  January 21, 2015
                        Due:  January 28, 2015

Homework is generally assigned on a Wednesday, and due nine days
later, on a Wednesday -- at the beginning of class.

This assignment is based on the material from Moore's Recursion and
Induction notes.  Please read the first six sections before attempting
to do the homework.

Your homework assignment is to provide solutions for problems 1 -- 17.



We will be using the ACL2 theorem-proving system starting in a couple
of weeks.

The top-level ACL2 webpage can be found here:

  http://www.cs.utexas.edu/users/moore/acl2/

If you wish to use this system on UTCS Linux-based computers, then be
sure that you have appropriate usage privileges.  Once you have logged
into a UTCS Linux-based computer, then you may type:

  /p/bin/acl2



If you wish to use ACL2 on your personal laptop, then you will need to
follow ACL2 installation instructions:

  http://www.cs.utexas.edu/users/moore/acl2/v7-0/HTML/installation/installation.html

Before ACL2 can be built on your laptop or deskside computer, you will
need to obtain a Lisp implementation.  We strongly recommend that you
use Clozure Common Lisp.  Why?  This is the Lisp that we generally
use.  This hashtag contains a bit of information that might be
helpful.


  http://www.cs.utexas.edu/users/moore/acl2/v7-0/HTML/installation/requirements.html#Obtaining-CCL



NOTE: We (either Nathan or Warren) will be available each week on
Monday, Tuesday, Wednesday, and Thursday from 2 to 3:30 pm in GDC
7.808.  If you don't see us there, come down the hall to our office
and ask us for help.  In addition, we can be available at other time
by appointment.  Don't wait if you have a problem -- come see us, and
we will try to help you.