This is an example from the textbook about Recursive Program Construction. I don’t understand how the second step of zap_2 was obtained. Specifically, why did x change to be between 2 and 0? And where did t^prime = t + x come from?

# Question from the textbook

**hehner**#2

Your question is how do we go from

(0) if x=0 then y:= 0 else x:= x–1. t:= t+1. zap_1 fi

to

(1) 0≤x<2 ⇒ xʹ=yʹ=0 ∧ tʹ=t+x

I admit, it is not obvious. You can test it by choosing various values for x and x’ and t and t’. Here’s how I probably got it. I simplified (0) as much as I could, and got

(2) (x=0 ⇒ x’=y’=0 ∧ t’=t) ∧ (x=1 ⇒ x’=y’=0 ∧ t’=t+1)

Maybe I still didn’t see that (2)=(1) so I found zap_3 and got

(3) (x=0 ⇒ x’=y’=0 ∧ t’=t) ∧ (x=1 ⇒ x’=y’=0 ∧ t’=t+1) ∧ (x=2 ⇒ x’=y’=0 ∧ t’=t+2)

Maybe then I could see that zap_n is

(4) 0≤x<n ⇒ xʹ=yʹ=0 ∧ tʹ=t+x

so I went back and wrote (1) for zap_2. I hope that answers.