n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
z:{1...}, s:({1...z}
{1...n}Peg).
Thm* (s is a Hanoi(n disk) seq on 1..z & s(1) = (
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:
, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z
Thm*
Thm* (
f:(PegPeg).
Thm* (Inj(Peg; Peg; f)
(x,i. f(s(x,i))) is a Hanoi(n disk) seq on a..z)p,r,q,s:Peg. p q r s Inj(Peg; Peg; permute(p to r ; q to s))n:, a,z,d:, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z
Thm*
Thm* (
x.s(x-d)) is a Hanoi(n disk) seq on a+d..z+dn:
, 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)
p,r,q,s:Peg. p q r s permute(p to r ; q to s)(q) = sp,r,q,s:Peg. p q r s permute(p to r ; q to s)(p) = rn:, 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)