At: next config wf 1
1. M: PM{i}
2. C: 
(M)
(
G(M))
let delta = 
(M)( < C.st,C.tape(C.hd) > ) in
< 1of(delta)
,(
z.if z=
C.hd
1of(2of(delta)) else C.tape(z) fi)
,if 2of(2of(delta)) C.hd+1 else C.hd-1 fi >
(M)(G(M))
By:
Analyze 2
THEN
Analyze 3
THEN
Reduce 0
Generated subgoals:None