1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:, z:{a...}, s:({a...z}{1...n1}Peg).
2. ((s is a Hanoi(n1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q)
2. ((
2. (((2^n1)z-a+1))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
7. z : {a...}
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. n  0
  2(2^(n-1))z-a+1

By:

Inst:  Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:, z:{a...}, s:({a...z}{1...n}Peg). Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q) Thm*  ( Thm*  ((x:{a...z-1}, y:{x+1...z}, p',q':Peg. Thm*  (((u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q) Thm*  ((& s(x) = (i.p')  {1...n-1}Peg & s(y) = (i.q')  {1...n-1}Peg Thm*  ((& p  p' Thm*  ((& q  q')) Using:[n | p | q | a | z | s] THEN ExistHD Hyp:-1

1

13. x : {a...z-1} 14. y : {x+1...z} 15. p' : Peg 16. q' : Peg 17. u:{a...x}. s(u,n) = p 18. u:{y...z}. s(u,n) = q 19. s(x) = (i.p')  {1...n-1}Peg 20. s(y) = (i.q')  {1...n-1}Peg 21. p  p' 22. q  q'   2(2^(n-1))z-a+1

12 steps

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