1. n : 
2. a : 
3. z : 
4. m : {a...z-1}
5. s1 : {a...m}{1...n}Peg
6. s2 : {m+1...z}{1...n}Peg
7. k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1)
8. s1 is a Hanoi(n disk) seq on a..m
9. s2 is a Hanoi(n disk) seq on m+1..z
10. x : {a...z}
11. x' : {a...z}
12. x+1 = x'
13. x = m
  k:{1...n}. Moving disk k of n takes (s1 @(m) s2)(x) to (s1 @(m) s2)(x')

By:	Rewrite by Thm*  n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg), Thm*  x:{a...m}. (s1 @(m) s2)(x) = s1(x) Using:[x:= x] THEN Rewrite by Thm*  n:, m,a,z:, s1:({a...m}{1...n}Peg), s2:({m+1...z}{1...n}Peg), Thm*  x:{m+1...z}. (s1 @(m) s2)(x) = s2(x) Using:[x:= x']

1

k:{1...n}. Moving disk k of n takes s1(x) to s2(x')

1 step

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