Near the end of Section 4.4, the text reads (sorry for cut/paste malfunctions): "Formula Spec is defined to equal Init ^ 2 [Next ]vars , where vars is defined to be the pair <x ; y> of the algorithm's variables."
Should this say "… where vars is defined to be the triple <x, y, pc> …"
As that's how "vars" is defined earlier in the spec.
Kevin