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*  ((HanoiHelper(n; s1; f; s2; g)/r1,r2.
Thm*  (((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g))

is based on that of

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)

Gloss

from which the program HanoiHelper(n; s1; f; s2; g) was derived as a realizer.

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