Nuprl - HanoiTowers LEMMAs for hanoi_sol2_ala

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

Rank	Theorem	Name
2	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]
cites the following:
1	Thm* x,y:Peg. x y x otherPeg(x; y)	[hanoi_otherpeg_diff3]
1	Thm* x,y:Peg. x y otherPeg(x; y) y	[hanoi_otherpeg_diff2]

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