1. n : 
2. n1:. 
2. n1<n
2. 
2. (p,q:Peg.
2. (p  q
2. (
2. ((a:. 
2. ((1of(HanoiSTD(n1 disks; from: p; to: q; indexing from: a)) = a+(2^n1)-1))
3. p : Peg
4. q : Peg
5. p  q
6. a : 
7. n  0
  1of(HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.
  HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)/z,s2.
  <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>)
  =
  a+2(2^(n-1))-1

By:	Inst: Thm*  x,y:Peg. x  y  x  otherPeg(x; y) Using:[p | q] THEN Inst: Thm*  x,y:Peg. x  y  otherPeg(x; y)  y Using:[p | q]

1

8. p  otherPeg(p; q) 9. otherPeg(p; q)  q   1of(HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1.   HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1)/z,s2.   <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2>)   =   a+2(2^(n-1))-1

3 steps

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