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))n:, f,g:({1...n}Peg), a:.
Thm*
z:{a...}, s:({a...z}{1...n}Peg).
Thm* s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g