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
i,j:. i<j 
i = j i>jn:, 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)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)