is mentioned by
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() Thm* (s is a Hanoi(n disk) seq on a..z & s(a) = ( ![]() ![]() Thm* ( ![]() ![]() Thm* ((2^n) ![]() | [hanoi_sol2_lb] |
![]() ![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() Thm* (s is a Hanoi(n disk) seq on a..z & s(a) = ( ![]() ![]() Thm* ( ![]() ![]() Thm* (( ![]() Thm* ((( ![]() ![]() Thm* ((& s(x) = ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ((& p ![]() Thm* ((& q ![]() | [hanoi_sol2_analemma] |
![]() ![]() 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] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | [exponentiation_wf_nat_plus] |
![]() ![]() ![]() ![]() | [exponentiation_wf_nat] |
![]() ![]() ![]() ![]() ![]() | [exponentiation_wf] |
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (s is a Hanoi(n disk) seq on a..z & s(a) = ( ![]() ![]() | [hanoi_sol2_via_general] |
![]() ![]() ![]() ![]() ![]() Thm* ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g | [hanoi_general_exists] |
![]() ![]() 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] |
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_sol2_ala_generalPROG_wf] |
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (s is a Hanoi(n disk) seq on a..z & s(a) = ( ![]() ![]() | [hanoi_sol2_ala_general] |
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() Thm* (s is a Hanoi(n disk) seq on 1..z & s(1) = ( ![]() ![]() | [hanoi_sol2_via_permshift] |
![]() ![]() ![]() ![]() ![]() ![]() 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] |
![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* HanoiHelper(n; s1; f; s2; g) Thm* ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_general_exists_lemma2PROG_wf] |
![]() ![]() ![]() ![]() ![]() ![]() 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* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ((r1 @(m) r2) is a Hanoi(n disk) seq on a..z & r1(a) = f & r2(z) = g) | [hanoi_general_exists_lemma2] |
![]() ![]() ![]() ![]() ![]() Thm* f(n) = g(n) Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* (( ![]() ![]() ![]() ![]() ![]() Thm* ((s is a Hanoi(n-1 disk) seq on a..z Thm* ((& s(a) = f ![]() ![]() ![]() Thm* ((& s(z) = g ![]() ![]() ![]() Thm* ( ![]() ![]() Thm* (( ![]() ![]() ![]() ![]() ![]() Thm* ((s is a Hanoi(n disk) seq on a..z & s(a) = f & s(z) = g)) | [hanoi_general_exists_lemma1] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() ![]() ![]() ![]() ![]() Thm* ( ![]() Thm* ![]() ![]() Thm* s1 is a Hanoi(n disk) seq on a..m Thm* ![]() ![]() Thm* s2 is a Hanoi(n disk) seq on m+1..z Thm* ![]() ![]() Thm* (s1 @(m) s2) is a Hanoi(n disk) seq on a..z | [hanoi_seq_join_seq] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() | [hanoi_seq_join_part2] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ![]() | [hanoi_seq_join_part1] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* (s1 @(m) s2) ![]() ![]() ![]() ![]() ![]() | [hanoi_seq_join_wf] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z Thm* ![]() ![]() Thm* ( ![]() Thm* ![]() ![]() Thm* s is a Hanoi(n' disk) seq on a..z | [hanoi_seq_shallower] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z Thm* ![]() ![]() Thm* ( ![]() | [hanoi_subseq] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z Thm* ![]() ![]() Thm* ( ![]() | [hanoi_seq_shift] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* n ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* (s is a Hanoi(n disk) seq on a..z Thm* ( ![]() ![]() Thm* ((s(?) {to n} ![]() | [hanoi_seq_deepen_seq] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* n ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* (i ![]() ![]() ![]() ![]() ![]() | [hanoi_seq_deepen_loweq] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* n ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* (n<i ![]() ![]() ![]() ![]() | [hanoi_seq_deepen_higheq] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* n ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_seq_deepen_wf] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* (Inj(Peg; Peg; f) ![]() ![]() ![]() | [hanoi_seq_permutepegs] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z Thm* ![]() ![]() Thm* ( ![]() Thm* (( ![]() Thm* ( ![]() ![]() Thm* (s is a Hanoi(n' disk) seq on a'..z') | [hanoi_seq_core] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z ![]() | [hanoi_seq_wf] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g ![]() ![]() ![]() | [hanoi_step_at_diff] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g ![]() ![]() | [hanoi_step_at_sym] |
![]() ![]() ![]() ![]() Thm* ( ![]() Thm* ![]() ![]() Thm* f(j) ![]() ![]() ![]() | [hanoi_step_at_change] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g ![]() ![]() ![]() ![]() ![]() | [hanoi_step_at_unique] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g Thm* ![]() ![]() Thm* f = ( ![]() ![]() ![]() ![]() | [hanoi_step_at_otherpeg] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g ![]() ![]() ![]() | [hanoi_step_at_change2] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g ![]() ![]() ![]() ![]() ![]() | [hanoi_step_at_same] |
![]() ![]() ![]() ![]() Thm* Moving disk k of n takes f to g ![]() | [hanoi_step_at_wf] |
![]() ![]() ![]() ![]() ![]() Thm* n ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* (n<i ![]() ![]() ![]() | [hanoi_extend_higheq] |
![]() ![]() ![]() ![]() ![]() Thm* n ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* (i ![]() ![]() ![]() ![]() | [hanoi_extend_loweq] |
![]() ![]() ![]() ![]() ![]() Thm* n ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_extend_wf] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_peg_perm_comp2] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_peg_perm_comp1] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_peg_perm_is_inj] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_peg_perm_wf] |
![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_diff4] |
![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_diff3] |
![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_diff2] |
![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_diff1] |
![]() ![]() ![]() ![]() | [hanoi_otherpeg_sym] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_only] |
![]() ![]() ![]() ![]() ![]() | [hanoi_otherpeg_wf] |
![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() ![]() Thm* (f(a) = p & f(z) = q Thm* ( ![]() ![]() Thm* (( ![]() Thm* ((( ![]() Thm* ((& f(x+1) ![]() Thm* ((& f(y-1) ![]() Thm* ((& ( ![]() | [hanoi_pegseq_analemma] |
![]() ![]() ![]() ![]() | [eq_hanoi_PEG_wf] |
Def == ![]() Def == x+1 = x' ![]() ![]() ![]() | [hanoi_seq] |
Def == ( ![]() ![]() ![]() ![]() ![]() Def == & ( ![]() ![]() ![]() ![]() ![]() | [hanoi_step_at] |
In prior sections: core fun 1 well fnd int 1 bool 1 int 2
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html