1. n : 
2. p : Peg
3. q : Peg
4. p  q
5. a : 
6. z : {a...}
7. f:({a...z}Peg). 
7. f(a) = p & f(z) = q
7. 
7. (x:{a...z-1}, y:{x+1...z}.
7. ((u:{a...x}. f(u) = p) & f(x+1)  p & f(y-1)  q & (u:{y...z}. f(u) = q))
8. s : {a...z}{1...n}Peg
9. s is a Hanoi(n disk) seq on a..z
10. s(a) = (i.p)
11. s(z) = (i.q)
  s(a,n) = p

None

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