(4steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Moving one disk changes its peg.

At: hanoi step at change2


  n:f,g:({1...n}Peg), k:{1...n}.
  Moving disk k of n takes f to g  f(k g(k)


By: Auto


Generated subgoal:

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)

3 steps

About:
natural_numberapplyfunctionimpliesall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions HanoiTowers Sections NuprlLIB Doc