Suppose the question asked you to show that

\forall x\forall y\forall z ((x + y) * z = (x * z) + (y * z))

First of all, you are allowed to shorten this to a proof of simply

(x + y) * z = (x * z) + (y * z)

thereby eliminating three proof boxes.

Now, say you choose to do this proof by induction on y.  Then your proof
should have the following general form (where the line numbers are made up
arbitrarily in this example; and view with a fixed-width font):

  ...
7.  (x + 0) * z = (x * z) + (0 * z)   (---some justification---)

+-----------------------------------------------------------------+
| y_0                                                             |
| +-------------------------------------------------------------+ |
| | 8.  (x + y_0) * z = (x * z) + (y_0 * z)   assumption        | |
| |                                                             | |
| |   ...                                                       | |
| |                                                             | |
| | 19. (x + (y_0 + 1) * z) = (x * z) + ((y_0 + 1) * z)  (----) | |
| +-------------------------------------------------------------+ |
| 20.  ((x + y_0) * z = (x * z) + (y_0 * z)) ->                   |
|       (x + (y_0 + 1) * z) = (x * z) + ((y_0 + 1) * z)  ->i 8-19 |
+-----------------------------------------------------------------+
21. \forall y(((x + y) * z = (x * z) + (y * z)) ->
        (x + (y + 1) * z) = (x * z) + ((y + 1) * z)) forall-i 8-20
22. (x + y) * z = (x * z) + (y * z)                  induction (or P3) 7, 21

For the bonus marks associated with a formal solution, you must handle the
quantifiers on x, y, and z properly.

To make use of an axiom:  Say you want to use P5 to show that

x + ((y + y) + 1) = (x + (y + y)) + 1

Formally, you must do the following:

15.  forall m(m + ((y + y) + 1) = (m + (y + y)) + 1)   \forall-e P5
16.  x + ((y + y) + 1) = (x + (y + y)) + 1             \forall-e 16

Informally, we will allow simply

15.  x + ((y + y) + 1) = (x + (y + y)) + 1   P5

The same guidelines apply for making use of previously-proved results.
Formally, you must carefully strip the quantifiers off.  Informally, just
do it and cite the axiom as justification.

Finally, I will allow you to make use of symmetry and transitivity for
equality.  So, for example, the following sequences are acceptable:

15.  a = b    (---some justification---)
16.  b = a    symmetry 15

8.  a = b   (---some justification---)
9.  b = c   (---some other justification---)
10. a = c   transitivity 8, 9

You may do this in both formal and informal contexts.  This is as much to
help the markers out as it is to help you out, because the alternative would
require more equality eliminations, and these are difficult to read and write.

In summary, you are allowed to make the simplifications outlined above to
shorten your proofs on this assignment.  If you want the extra marks for
formality, then you must do the following:

  * explicitly introduce and eliminate all quantifiers.
  * do not use the "______ to both sides" justification.

Be sure, if you do this, that you do it carefully, or you risk losing marks on
the original question.