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'))p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:, z:{a...}, f:({a...z}Peg).
Thm* (f(a) = p & f(z) = q
Thm* (
Thm* ((
x:{a...z-1}, y:{x+1...z}.
Thm* (((
u:{a...x}. f(u) = p)
Thm* ((& f(x+1)
p
Thm* ((& f(y-1)
q
Thm* ((& (
u:{y...z}. f(u) = q)))n:, f,g:({1...n}Peg), j:{1...n}.
Thm* (
k:{1...n}. Moving disk k of n takes f to g)
Thm*
Thm* f(j)
g(j) Moving disk j of n takes f to gx,y:Peg. x y otherPeg(x; y) = otherPeg(y; x)n:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g
Thm*
Thm* f = (
i.otherPeg(f(k); g(k))) {1...k-1}Pegn:, f,g:({1...n}Peg), k:{1...n}.
Thm* Moving disk k of n takes f to g
Moving disk k of n takes g to fx,y:Peg. x y x otherPeg(x; y)x,y:Peg. x y y otherPeg(x; y)