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

By:	BackThru: Thm*  x,y:Peg. x  y  otherPeg(x; y)  y

None

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