(7steps total)
PfGloss
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Permuting the pegs throughout a Hanoi sequence results in a Hanoi sequence.
At:
hanoi
seq
permutepegs
n
:
,
a
,
z
:
,
s
:({
a
...
z
}
{1...
n
}
Peg).
s
is a Hanoi(
n
disk) seq on
a
..
z
(
f
:(Peg
Peg).
(
Inj(Peg; Peg;
f
)
(
x
,
i
.
f
(
s
(
x
,
i
))) is a Hanoi(
n
disk) seq on
a
..
z
)
By:
Auto
Generated subgoal:
1
1.
n
:
2.
a
:
3.
z
:
4.
s
: {
a
...
z
}
{1...
n
}
Peg
5.
s
is a Hanoi(
n
disk) seq on
a
..
z
6.
f
: Peg
Peg
7. Inj(Peg; Peg;
f
)
(
x
,
i
.
f
(
s
(
x
,
i
))) is a Hanoi(
n
disk) seq on
a
..
z
6
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PfGloss
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc