We are left only with showing (C). Backing through the lemma

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

our problem reduces to showing the three premises of that lemma, two of which are immediately solved by

Thm*  a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm*  nn'
Thm*  
Thm*  (h:({n+1...n'}Peg). 
Thm*  (s is a Hanoi(n disk) seq on a..z
Thm*  (
Thm*  ((s(?) {to n}  h {to n'}) is a Hanoi(n' disk) seq on a..z)

leaving us to show only that

k:{1...n}. 
Moving disk k of n
takes (s1(?) {to n-1}  f {to n})(m) to (s2(?) {to n-1}  g {to n})(m+1)

Obviously we should move the largest disk (n), and expanding the definition of moving a disk leaves us with two goals

(D) i:{1...n}. 
(D) (s1(?) {to n-1}  f {to n})(m,i) = (s2(?) {to n-1}  g {to n})(m+1,i)
(D) 
(D) i  n

(E) i:{1...n-1}. 
(E) (s1(?) {to n-1}  f {to n})(m,i)  (s1(?) {to n-1}  f {to n})(m,n)
(E) & (s2(?) {to n-1}  g {to n})(m+1,i)  (s2(?) {to n-1}  g {to n})(m+1,n)

To show (D) we case split on whether i = n. If i = n then

(s1(?) {to n-1}  f {to n})(m,i) = (s2(?) {to n-1}  g {to n})(m+1,i)

simplifies to f(i) = g(i) and rewriting i to n reduces our goal (D) to

f(n) = g(n)  n  n

which follows from our assumption that f(n)  g(n). If i  n then

(s1(?) {to n-1}  f {to n})(m,i) = (s2(?) {to n-1}  g {to n})(m+1,i)

simplifies to s1(m,i) = s2(m+1,i), which follows from our assumption that s1(m) = s2(m+1).

Turning to (E),

(s1(?) {to n-1}  f {to n})(m,i) simplifies to s1(m,i)

(s2(?) {to n-1}  g {to n})(m+1,i) simplifies to s2(m+1,i)

(s1(?) {to n-1}  f {to n})(m,n) simplifies to f(n)

(s2(?) {to n-1}  g {to n})(m+1,n) simplifies to g(n)

reducing (E) to s1(m,i)  f(n) and s2(m+1,i)  g(n), which follow from ousr assumption that

i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n).

QED

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