is mentioned by

Thm*  n:, p,q:Peg. Thm*  p  q Thm*   Thm*  (a:.  Thm*  (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm*  (= Thm*  ((HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1. Thm*  ((HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1) Thm*  ((/z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>))	[hanoi_sol2_ala_generalPROGcomp]
Thm*  n:, f,g:({1...n}Peg), k:{1...n}. Thm*  Moving disk k of n takes f to g Thm*   Thm*  f = (i.otherPeg(f(k); g(k)))  {1...k-1}Peg	[hanoi_step_at_otherpeg]
Thm*  x,y:Peg. x  y  y  otherPeg(x; y)	[hanoi_otherpeg_diff4]
Thm*  x,y:Peg. x  y  x  otherPeg(x; y)	[hanoi_otherpeg_diff3]
Thm*  x,y:Peg. x  y  otherPeg(x; y)  y	[hanoi_otherpeg_diff2]
Thm*  x,y:Peg. x  y  otherPeg(x; y)  x	[hanoi_otherpeg_diff1]
Thm*  x,y:Peg. x  y  otherPeg(x; y) = otherPeg(y; x)	[hanoi_otherpeg_sym]
Thm*  x,y,z:Peg. x  y  x  z  y  z  x = otherPeg(y; z)	[hanoi_otherpeg_only]
Def  HanoiSTD(n disks; from: p; to: q; indexing from: a) Def  == if n=0 <a,x,i. whatever> Def  == else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) Def  == else /m,s1. Def  == else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m Def  == else HanoiSTD(+1) Def  == else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi Def  (recursive)	[hanoi_sol2_ala_generalPROG]
Def  permute(p to r ; q to s)(u) == if u=p r ; u=q s else otherPeg(r; s) fi	[hanoi_peg_perm]

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