First Printing (1996)

The following Postscript file contains the corrections displayed above: Errata.ps.

The following pages contain corrections to the first printing, and are incorporated in the second printing:
Page028.ps Page069.ps Page136.ps Page150.ps Page160.ps Page251.ps Page255.ps.

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.