1. n : 
2. a : 
3. z : 
4. s : {a...z}{1...n}Peg
5. s is a Hanoi(n disk) seq on a..z
6. f : PegPeg
7. Inj(Peg; Peg; f)
8. (x,i. f(s(x,i)))  {a...z}{1...n}Peg
9. x : {a...z}
10. x' : {a...z}
11. x+1 = x'
12. k : {1...n}
13. Moving disk k of n takes s(x) to s(x')
  Moving disk k of n takes i.f(s(x,i)) to i.f(s(x',i))

1	13. i : {1...n} 14. f(s(x,i)) = f(s(x',i))   s(x,i) = s(x',i)	1 step
2	13. i : {1...n} 14. i  k 15. s(x,i) = s(x',i)   f(s(x,i)) = f(s(x',i))	1 step
3	13. i : {1...k-1} 14. f(s(x,i)) = f(s(x,k))   s(x,i) = s(x,k)	1 step
4	13. i : {1...k-1} 14. f(s(x',i)) = f(s(x',k))   s(x',i) = s(x',k)	1 step

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