1. n : 
2. p : Peg
3. q : Peg
4. p  q
5. a : 
6. z : {a...}
7. f:({a...z}Peg). 
7. f(a) = p & f(z) = q
7. 
7. (x:{a...z-1}, y:{x+1...z}.
7. ((u:{a...x}. f(u) = p) & f(x+1)  p & f(y-1)  q & (u:{y...z}. f(u) = q))
8. s : {a...z}{1...n}Peg
9. s is a Hanoi(n disk) seq on a..z
10. s(a) = (i.p)
11. s(z) = (i.q)
12. x : {a...z-1}
13. y : {x+1...z}
14. u:{a...x}. s(u,n) = p
15. s(x+1,n)  p
16. s(y-1,n)  q
17. u:{y...z}. s(u,n) = q
  s(x,n)  s(x+1,n) & s(y-1,n)  s(y,n)

By:	SimilarTo: s(x+1,n)  p  Peg & s(y-1,n)  q  Peg

1	18. s(x,n) = s(x+1,n)   s(x+1,n) = p	1 step
2	18. s(y-1,n) = s(y,n)   s(y-1,n) = q	1 step

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