(2steps total)
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi
peg
perm
comp1
p
,
r
,
q
,
s
:Peg.
p
q
r
s
permute(
p
to
r
;
q
to
s
)(
p
) =
r
By:
Compute
Co
permute(
p
to
r
;
q
to
s
)(
p
) *
if
p
=
p
r
;
p
=
q
s
else otherPeg(
r
;
s
) fi
Generated subgoal:
1
1.
p
: Peg
2.
r
: Peg
3.
q
: Peg
4.
s
: Peg
5.
p
q
6.
r
s
if
p
=
p
r
;
p
=
q
s
else otherPeg(
r
;
s
) fi =
r
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