n:
, a:
, z:{a...}, m:{a...z-1}, f,g:({1...n}
Peg).
f(n) 
g(n)
(s1:({a...m}{1...n-1}Peg), s2:({m+1...z}{1...n-1}Peg).
(s1 is a Hanoi(n-1 disk) seq on a..m
(& s1(a) = f 
{1...n-1}Peg
(& s2 is a Hanoi(n-1 disk) seq on m+1..z
(& s2(z) = g {1...n-1}Peg
(& s1(m) = s2(m+1)
(& (i:{1...n-1}. s1(m,i) f(n) & s2(m+1,i) g(n))
(
((HanoiHelper(n; s1; f; s2; g)/r1,r2.
(((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g))| By: |
|
| 1 |
2. a :
3. z : {a...} 4. m : {a...z-1} 5. f : {1...n} Peg
6. g : {1...n} Peg
7. f(n) g(n)
8. s1 : {a...m} {1...n-1}Peg
9. s2 : {m+1...z} {1...n-1}Peg
10. s1 is a Hanoi(n-1 disk) seq on a..m 11. s1(a) = f {1...n-1}Peg
12. s2 is a Hanoi(n-1 disk) seq on m+1..z 13. s2(z) = g {1...n-1}Peg
14. s1(m) = s2(m+1) 15. i:{1...n-1}. s1(m,i) f(n) & s2(m+1,i) g(n)
HanoiHelper(n; s1; f; s2; g)/r1,r2.
(r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g | 25 steps |
About:
 |  |  |  |  |  |
 |  |  |  |  |