is mentioned by
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* (1of(HanoiSTD(n disks; from: p; to: q; indexing from: a)) = a+(2^n)-1) | [hanoi_general_exists_lemma2PROG_endpoint] |
![]() ![]() 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] |
![]() ![]() ![]() 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] |
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html