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* ((HanoiHelper(n; s1; f; s2; g)/r1,r2.
Thm* (((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g))
n:, a,z:, m:{a...z-1}, s1:({a...m}{1...n}Peg),
Thm*
s2:({m+1...z}{1...n}Peg).
Thm* (
k:{1...n}. Moving disk k of n takes s1(m) to s2(m+1))
Thm*
Thm* s1 is a Hanoi(n disk) seq on a..m
Thm*
Thm* s2 is a Hanoi(n disk) seq on m+1..z
Thm*
Thm* (s1 @(m) s2) is a Hanoi(n disk) seq on a..z
a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg).
Thm* (s is a Hanoi(n disk) seq on a..z
Thm* (
Thm* ((s(?) {to n}
h {to n'}) is a Hanoi(n' disk) seq on a..z)a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg), i:{1...n'}.
Thm* (i
n (x:{a...z}. (s(?) {to n} h {to n'})(x,i) = s(x,i)))a,z:, n:, s:({a...z}{1...n}Peg), n':.
Thm* n
n'
Thm*
Thm* (
h:({n+1...n'}Peg), i:{1...n'}.
Thm* (n<i
(x:{a...z}. (s(?) {to n} h {to n'})(x,i) = h(i)))