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

1

9. f(i) = g(i)  i  k   i = k

1 step

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