Example in Ch 9.1.7

[lemirand]

I’m a little confused on the transition from the third line to the fourth line. When eliminating the quantifier, what happened to w’ and r’? I understand how x’=M_0 became x’=2, but w’ and r’ were initially 0 and became 1, so they didn’t remain unchanged.

Is it because r and w are local variables?

[hehner]

You have answered your own question: yes, it is because r and w are local variables, so when we get rid of var r, w: xnat, they disappear.

I see that there is a typo in this calculation. It says r’:= r+1. That should be just r’ = r+1. It’s the only typo or error of any kind in the whole book! And you found it! I’ll fix it today.