Rank | Theorem | Name |
4 | ![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a)/z,s. Thm* (s is a Hanoi(n disk) seq on a..z Thm* (& s(a) = ( ![]() ![]() ![]() ![]() Thm* (& s(z) = ( ![]() ![]() ![]() ![]() | [hanoi_sol2_ala_generalPROGworks] |
cites the following: | ||
1 | ![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_diff3] |
1 | ![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_diff2] |
2 | ![]() ![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm* (= Thm* ((HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a)/m,s1. Thm* ((HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m+1) Thm* ((/z,s2. <z,HanoiHelper(n; s1; ![]() ![]() | [hanoi_sol2_ala_generalPROGcomp] |
0 | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() | [hanoi_seq_join_part2] |
0 | ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() | [hanoi_seq_join_part1] |
3 | ![]() ![]() ![]() ![]() ![]() ![]() Thm* f(n) ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* (s1 is a Hanoi(n-1 disk) seq on a..m Thm* (& s1(a) = f ![]() ![]() ![]() Thm* (& s2 is a Hanoi(n-1 disk) seq on m+1..z Thm* (& s2(z) = g ![]() ![]() ![]() Thm* (& s1(m) = s2(m+1) Thm* (& ( ![]() ![]() ![]() Thm* ( ![]() ![]() Thm* ((HanoiHelper(n; s1; f; s2; g)/r1,r2. Thm* (((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g)) | [hanoi_general_exists_lemma2PROGworks] |