n':
, n:{n'...}, a,z:
, s:({a...z}
{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z
Thm*
Thm* (
a',z':{a...z}.
Thm* ((
x:{a'...z'}, i:{n'+1...n}. s(a',i) = s(x,i))
Thm* (
Thm* (s is a Hanoi(n' disk) seq on a'..z')
n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g
f(k) 
g(k)