1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (a:. 
3. (HanoiSTD(n-1 disks; from: p; to: q; indexing from: a)/z,s.
3. (s is a Hanoi(n-1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. a : 
8. p = otherPeg(p; q)
9. otherPeg(p; q) = q
10. m : {a...}
11. s1 : {a...m}{1...n-1}Peg
12. <m,s1> = HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)
13. s1 is a Hanoi(n-1 disk) seq on a..m
14. s1(a) = (i.p)
15. s1(m) = (i.otherPeg(p; q))
16. z : {m+1...}
17. s2 : {m+1...z}{1...n-1}Peg
18. <z,s2>
18. =
18. HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)
19. s2 is a Hanoi(n-1 disk) seq on m+1..z
20. s2(m+1) = (i.otherPeg(p; q))
21. s2(z) = (i.q)
22. r1 : {a...m}{1...n}Peg
23. r2 : {m+1...z}{1...n}Peg
24. <r1,r2> = HanoiHelper(n; s1; i.p; s2; i.q)
  HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2.
  (r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = (i.p) & r2(z) = (i.q)

By:

BackThru:  Thm*  n:, a:, z:{a...}, m:{a...z-1}, f,g:({1...n}Peg). Thm*  f(n)  g(n) Thm*   Thm*  (s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg). Thm*  (s1 is a Hanoi(n-1 disk) seq on a..m Thm*  (& s1(a) = f  {1...n-1}Peg Thm*  (& s2 is a Hanoi(n-1 disk) seq on m+1..z Thm*  (& s2(z) = g  {1...n-1}Peg Thm*  (& s1(m) = s2(m+1) Thm*  (& (i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n)) Thm*  ( Thm*  ((HanoiHelper(n; s1; f; s2; g)/r1,r2. Thm*  (((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g)) THEN Reduce Concl

1	25. i : {1...n-1}   s1(m,i)  p	2 steps
2	25. i : {1...n-1}   s2(m+1,i)  q	1 step

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