n:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:
.
Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.
Thm* (s is a Hanoi(n disk) seq on a..z
Thm* (& s(a) = (
i.p) 
{1...n}
Peg
Thm* (& s(z) = (
i.q) {1...n}Peg)x,y:Peg. x y x otherPeg(x; y)x,y:Peg. x y otherPeg(x; y) yn:
, p,q:Peg.
Thm* p
q
Thm*
Thm* (
a:.
Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a)
Thm* (=
Thm* ((HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.
Thm* ((HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)
Thm* ((/z,s2. <z,HanoiHelper(n; s1;
i.p; s2; i.q)/r1,r2. r1 @(m) r2>))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)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:, 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))