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?