By: |
Co1of(HanoiSTD(n disks; from: p; to: q; indexing from: a) Co1of(* Co1of(if n=0 <a,x,i. whatever> Co1of(else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) Co1of(else /m,s1. Co1of(else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1) Co1of(else /z,s2. <z,HanoiHelper(n; s1; i.p; s2; i.q)/r1,r2. r1 @(m) r2> fi) Co= Coa+(2^n * if n=0 1 else 2(2^(n-1)) fi)-1 Co THEN SplitITE Concl |
1 |
1of(<a,x,i. whatever>) = a+1-1 | 1 step |
2 |
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 | 4 steps |
About: