n:
, f,g:({1...n}
Peg), a:
.
Thm*
z:{a...}, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g
n:
, f,g:({1...n}Peg).
Thm* f(n) = g(n)
Thm*
Thm* (
a:, z:{a...}.
Thm* ((
s:({a...z}{1...n-1}Peg).
Thm* ((s is a Hanoi(n-1 disk) seq on a..z
Thm* ((& s(a) = f
{1...n-1}Peg
Thm* ((& s(z) = g
{1...n-1}Peg)
Thm* (
Thm* ((
s:({a...z}{1...n}Peg).
Thm* ((s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g))
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)
x,y:Peg. x y otherPeg(x; y) xx,y:Peg. x y otherPeg(x; y) yn:, 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)