Thm* n:
, p,q:Peg.
Thm* pq
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)
is based on that of
Thm* n:
, p,q:Peg.
Thm* pq
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))
from which the program
About:
![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() |
![]() |