1. n : 
2. 0<n
3. p,q:Peg.
3. p  q
3. 
3. (z:{1...}, s:({1...z}{1...n-1}Peg).
3. (s is a Hanoi(n-1 disk) seq on 1..z & s(1) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. p  q
7. p  otherPeg(p; q)
8. otherPeg(p; q)  q
9. m : {1...}
10. s1 : {1...m}{1...n-1}Peg
11. s1 is a Hanoi(n-1 disk) seq on 1..m
12. s1(1) = (i.p)
13. s1(m) = (i.otherPeg(p; q))
14. (x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x,i)))
14. is a Hanoi(n-1 disk) seq on 1..m
15. (x,i. permute(p to otherPeg(p; q) ; otherPeg(p; q) to q)(s1(x-m,i)))
15. is a Hanoi(n-1 disk) seq on 1+m..m+m
  z:{1...}, m:{1...z-1}, s1:({1...m}{1...n}Peg),
  s2:({m+1...z}{1...n}Peg).
  (s1 @(m) s2) is a Hanoi(n disk) seq on 1..z
  & s1(1) = (i.p)  {1...n}Peg
  & s2(z) = (i.q)

By:

Witness: m+m | m THEN 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*  (r1:({a...m}{1...n}Peg), r2:({m+1...z}{1...n}Peg). Thm*  ((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g) THEN Reduce Concl

1

s1:({1...m}{1...n-1}Peg), s2:({m+1...m+m}{1...n-1}Peg).   s1 is a Hanoi(n-1 disk) seq on 1..m   & s1(1) = (i.p)   & s2 is a Hanoi(n-1 disk) seq on m+1..m+m   & s2(m+m) = (i.q)   & s1(m) = s2(m+1)   & (i:{1...n-1}. s1(m,i)  p & s2(m+1,i)  q)

11 steps

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