(6steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Moving one disk leaves the smaller disks in place.

At: hanoi step at otherpeg

  n:, f,g:({1...n}Peg), k:{1...n}.
  Moving disk k of n takes f to g
  
  f = (i.otherPeg(f(k); g(k)))  {1...k-1}Peg
By: SimilarTo:
Thm*  n:, f,g:({1...n}Peg), k:{1...n}.
Thm*  Moving disk k of n takes f to g  f(k)  g(k)
THEN
New:i FunExtensionality

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
6. f(k)  g(k)
7. i : {1...k-1}
  f(i) = otherPeg(f(k); g(k))
5 steps

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

(6steps total) PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc