1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (z:{1...}, s:({1...z}{1...n-1}Peg).
3. (s is a Hanoi(n-1 disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. z : {1...}
8. m : {1...z-1}
9. s1 : {1...m}{1...n}Peg
10. s2 : {m+1...z}{1...n}Peg
11. (s1 @(m) s2) is a Hanoi(n disk) seq on 1..z
12. s1(1) = (i.p)
13. s2(z) = (i.q)
  z:{1...}, s:({1...z}{1...n}Peg).
  s is a Hanoi(n disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q)

1	(s1 @(m) s2)(1) = (i.p)	1 step
2	(s1 @(m) s2)(z) = (i.q)	1 step

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