(4steps total)
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi
step
at
change2
1
1.
n
:
2.
f
: {1...
n
}
Peg
3.
g
: {1...
n
}
Peg
4.
k
: {1...
n
}
5. Moving disk
k
of
n
takes
f
to
g
f
(
k
)
g
(
k
)
By:
Analyze-1
Generated subgoal:
1
5.
i
:{1...
n
}.
f
(
i
) =
g
(
i
)
i
k
6.
i
:{1...
k
-1}.
f
(
i
)
f
(
k
) &
g
(
i
)
g
(
k
)
f
(
k
)
g
(
k
)
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(4steps total)
PrintForm
Definitions
HanoiTowers
Sections
NuprlLIB
Doc
Peg
f(k) 
g(k)
i:{1...n}. f(i) = g(i) 
i 
