WhoCites
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(given distinct
Peg
s, the other (third) peg)
Who Cites hanoi
otherpeg?
hanoi_otherpeg
Def otherPeg(
x
;
y
) == 6-(
x
+
y
)
Thm*
x
,
y
:Peg.
x
y
otherPeg(
x
;
y
)
Peg
Syntax:
otherPeg(
x
;
y
)
has structure:
hanoi_otherpeg(
x
;
y
)
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
x,y:Peg. x 
y 
otherPeg(x; y) 
Pegx,y:Peg. x y otherPeg(x; y) Peg
