n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:
.
Thm* (
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))x,y:Peg. x y x otherPeg(x; y)x,y:Peg. x y otherPeg(x; y) yn:
, 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)
n:, 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)