(2steps total)
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi
extend
higheq
n
:
,
f
:({1...
n
}
Peg),
n'
:
.
n
n'
(
f'
:({
n
+1...
n'
}
Peg),
i
:{1...
n'
}.
(
n
<
i
(
f
{to
n
}
f'
{to
n'
})(
i
) =
f'
(
i
))
By:
Auto
Generated subgoal:
1
1.
n
:
2.
f
: {1...
n
}
Peg
3.
n'
:
4.
n
n'
5.
f'
: {
n
+1...
n'
}
Peg
6.
i
: {1...
n'
}
7.
n
<
i
(
f
{to
n
}
f'
{to
n'
})(
i
) =
f'
(
i
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc