Thm*  n:, a,z:, m:{a...z-1}, s1:({a...m}{1...n}Peg),
Thm*  s2:({m+1...z}{1...n}Peg).
Thm*  (k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1))
Thm*  
Thm*  s1 is a Hanoi(n disk) seq on a..m
Thm*  
Thm*  s2 is a Hanoi(n disk) seq on m+1..z
Thm*  
Thm*  (s1 @(m) s2) is a Hanoi(n disk) seq on a..z

We shall refer repeatedly to the definition of Hanoi sequence

Def  s is a Hanoi(n disk) seq on a..z
Def  == x,x':{a...z}.
Def  == x+1 = x'  (k:{1...n}. Moving disk k of n takes s(x) to s(x'))

Assuming that

(A) s1 is a Hanoi(n disk) seq on a..m

(B) s2 is a Hanoi(n disk) seq on m+1..z

(C) k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1)

the problem, expanding the definition of Hanoi sequence in the conclusion, is to show that at each step, x+1 = x', of the joined sequence,

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

which we proceed to do by cases: x<m, x = m, x>m. If x<m then 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)

(s1 @(m) s2)(x) and (s1 @(m) s2)(x') reduce to s1(x) and s1(x'), which makes (*) follow from (A) and the definition of Hanoi sequence. Similarly, if x>m then 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)

(s1 @(m) s2)(x) and (s1 @(m) s2)(x') reduce to s2(x) and s2(x'), which makes (*) follow from (B). Finally, if x = m then (s1 @(m) s2)(x) and (s1 @(m) s2)(x') reduce to s1(x) and s2(x'), since now x and x' fall on oppositie sides of the dividing line between the joined sequences, but since m+1 = x' the goal (*) now follows from (C).

QED

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