IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi peg perm comp2 p,r,q,s:Peg. pqrs permute(p to r ; q to s)(q) = s
By:
Compute
Copermute(p to r ; q to s)(q) * if q=pr ; q=qs else otherPeg(r; s) fi