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
  p',q':Peg.
  (u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)
  & s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg
  & p  p'
  & q  q'

By:	s(x,n)  s(x+1,n)  Peg & s(y-1,n)  s(y,n)  Peg  Asserted THEN (Inst: Hyp:9 Using:[x | x+1] THEN Inst: Hyp:9 Using:[y-1 | y])

1	s(x,n)  s(x+1,n) & s(y-1,n)  s(y,n)	3 steps
2	18. s(x,n)  s(x+1,n) 19. s(y-1,n)  s(y,n) 20. k:{1...n}. Moving disk k of n takes s(x) to s(x+1) 21. k:{1...n}. Moving disk k of n takes s(y-1) to s(y)   p',q':Peg.   (u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)   & s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg   & p  p'   & q  q'	15 steps

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