Definitions HanoiTowers Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Standard Solution made Explicit - continued from Standard Solution

The recursive procedure implicit in the last proof is: If there are no disks then we're done, otherwise, move the smaller disks according to this procedure to the peg other than the source and destination pegs, then move the largest disk to the destination peg, then move the smaller disks to the destination peg. The seqence of stacking situations described implicit in this proof can be defined explicitly as:

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)

Observe that this procedure for producing stacking situation sequences makes two recursive calls in it non-trivial branch. The result of the first call is split into its ending-point index and the function assigning stacking situations to indices. The second recursive call uses the index from the first call to calculate the starting index for the second call. The ending-point index returned from the second recursive call is used as the ending-point for the whole result, and the assignment function returned for the whole is gotten by chaining together two sequences provided by a call to an auxilliary procedure designed for this purpose.

Def  HanoiHelper(n; s1; f; s2; g)
Def  == <s1(?) {to n-1}  f {to n},s2(?) {to n-1}  g {to n}>

This procedure simply "Deepens" a couple of sequences. The definition of HanoiSTD(n disks; from: p; to: q; indexing from: a) was derived by following the proof of

Thm*  n:, p,q:Peg.
Thm*  p  q
Thm*  
Thm*  (a:. 
Thm*  (z:{a...}, s:({a...z}{1...n}Peg).
Thm*  (s is a Hanoi(n disk) seq on a..z & s(a) = (i.p) & s(z) = (i.q))

which was mentioned above, with the recursive calls corresponding to applications of the inductive hypothesis, and the call to HanoiHelper(n; s1; f; s2; g) corresponding to a citation in that proof of the special purpose lemma

Thm*  n:, a:, z:{a...}, m:{a...z-1}, f,g:({1...n}Peg).
Thm*  f(n)  g(n)
Thm*  
Thm*  (s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg).
Thm*  (s1 is a Hanoi(n-1 disk) seq on a..m
Thm*  (& s1(a) = f  {1...n-1}Peg
Thm*  (& s2 is a Hanoi(n-1 disk) seq on m+1..z
Thm*  (& s2(z) = g  {1...n-1}Peg
Thm*  (& s1(m) = s2(m+1)
Thm*  (& (i:{1...n-1}. s1(m,i)  f(n) & s2(m+1,i)  g(n)))
Thm*  
Thm*  (r1:({a...m}{1...n}Peg), r2:({m+1...z}{1...n}Peg).
Thm*  ((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g)

Continued at hanoi basic solution cont2

About:
pairspreadifthenelseintnatural_number
addsubtractlambdaapplyfunctionrecursive_def_notice
equalimpliesandallexists!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions HanoiTowers Sections NuprlLIB Doc