At: hanoi step at change

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

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

1

1. n :  2. f : {1...n}Peg 3. g : {1...n}Peg 4. j : {1...n} 5. k:{1...n}. Moving disk k of n takes f to g  f(j)  g(j)  j = k 6. k:{1...n}. Moving disk k of n takes f to g 7. f(j)  g(j)   Moving disk j of n takes f to g

3 steps

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