(7steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The standard Hanoi Towers solution is a sequence whose length is 2 raised to the number of disks.

At: hanoi general exists lemma2PROG endpoint

  n:, p,q:Peg.
  p  q
  
  (a:. 1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1)
By: CompNatInd Concl

Generated subgoal:

1 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 : 
  1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1
6 steps

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

(7steps total) PfGloss PrintForm Definitions Lemmas HanoiTowers Sections NuprlLIB Doc