First Printing (1996)

The following Postscript file contains the corrections displayed above:

The following pages contain corrections to the first printing, and are incorporated in the second printing:

First and Second Printing

The following are problems found in the second printing; they are also present in the first printing.

Page 71:
Following the method pred in the first definition of zero, there is a missing comma.
Thanks to Gary T. Leavens.
Page 137:
Rule (Red Select): the third premise (xj not in dom(S')) is simply redundant. (This redundancy is inconsistent with the formulation of rule (Red Let).)
Thanks to Gary T. Leavens.
Page 146:
The last two lines of section 11.3.2 should read:
p1.mv_x(-3); p1.x   =   0
p2.mv_x(-3); p2.x   =   0
Thanks to Jason M. Smith.

Second Printing (1998)

Page 136:
Rule (Stack x): the third premise (forall i in 1..n) is spurious and should be ignored.
Thanks to Gary T. Leavens.

Last updated April 27, 2000.

 Luca Cardelli