n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:
, z:{a...}, s:({a...z}
{1...n}Peg).
Thm* (s is a Hanoi(n disk) seq on a..z & s(a) = (
i.p) & s(z) = (i.q)
Thm* (
Thm* ((2^n)
z-a+1)n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:, z:{a...}, s:({a...z}{1...n}Peg).
Thm* (s is a Hanoi(n disk) seq on a..z & s(a) = (
i.p) & s(z) = (i.q)
Thm* (
Thm* ((
x:{a...z-1}, y:{x+1...z}, p',q':Peg.
Thm* (((
u:{a...x}. s(u,n) = p) & (u:{y...z}. s(u,n) = q)
Thm* ((& s(x) = (
i.p') 
{1...n-1}Peg & s(y) = (i.q') {1...n-1}Peg
Thm* ((& p
p'
Thm* ((& q
q'))n':, n:{n'...}, a:, z:{a...}, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z
Thm*
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:, 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}. s is a Hanoi(n disk) seq on a'..z')