1. a : 
2. z : 
3. n : 
4. s : {a...z}{1...n}Peg
5. n' : 
6. nn'
7. h : {n+1...n'}Peg
8. x : {a...z}
9. x' : {a...z}
10. x+1 = x'
11. k : {1...n}
12. Moving disk k of n takes s(x) to s(x')
  Moving disk k of n'
  takes (s(?) {to n}  h {to n'})(x) to (s(?) {to n}  h {to n'})(x')

1	12. i:{1...n}. s(x,i) = s(x',i)  i  k 13. i : {1...n'}   (s(?) {to n}  h {to n'})(x,i) = (s(?) {to n}  h {to n'})(x',i)  i  k	4 steps
2	12. i : {1...k-1} 13. s(x,i)  s(x,k) & s(x',i)  s(x',k)   (s(?) {to n}  h {to n'})(x,i)  (s(?) {to n}  h {to n'})(x,k)   & (s(?) {to n}  h {to n'})(x',i)  (s(?) {to n}  h {to n'})(x',k)	1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html