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
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'

By:	FwdThru:  Thm*  n:, f,g:({1...n}Peg), j:{1...n}. Thm*  (k:{1...n}. Moving disk k of n takes f to g) Thm*   Thm*  f(j)  g(j)  Moving disk j of n takes f to g on [ Hyp:20 ] Using:[j:= n]

1

22. Moving disk n of n takes s(x) to s(x+1)   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'

14 steps

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