IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hanoi sol2 ala generalPROGworks2 1. n : 2. 0<n 3. p,q:Peg.
3. pq 3. 3. (a:.
3. (HanoiSTD(n-1 disks; from: p; to: q; indexing from: a)/z,s.
3. (s is a Hanoi(n-1 disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))
4. p : Peg
5. q : Peg
6. pq 7. a : HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s.
s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) {1...n}Peg
& s(z) = (i.q) {1...n}Peg