At: hanoi step at unique

  n:, f,g:({1...n}Peg), i,k:{1...n}.
  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. i : {1...n} 5. k : {1...n} 6. i:{1...n}. f(i) = g(i)  i  k 7. i:{1...k-1}. f(i)  f(k) & g(i)  g(k) 8. f(i)  g(i)   i = k

2 steps

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