Some definitions of interest. | |
hanoi_seq | Def == ![]() Def == x+1 = x' ![]() ![]() ![]() |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* s is a Hanoi(n disk) seq on a..z ![]() | |
hanoi_PEG | |
![]() | |
hanoi_sol2_ala_generalPROG | Def == if n= ![]() ![]() ![]() Def == else HanoiSTD(n-1 disks; from: p; to: otherPeg(p; q); indexing from: a) Def == else /m,s1. Def == else HanoiSTD(n-1 disks; from: otherPeg(p; q); to: q; indexing from: m Def == else HanoiSTD(+1) Def == else /z,s2. <z,HanoiHelper(n; s1; ![]() ![]() Def (recursive) |
![]() ![]() Thm* p ![]() Thm* ![]() ![]() Thm* ( ![]() ![]() Thm* (HanoiSTD(n disks; from: p; to: q; indexing from: a) Thm* ( ![]() ![]() ![]() ![]() ![]() ![]() | |
int_iseg | ![]() ![]() ![]() |
![]() ![]() ![]() | |
nat | ![]() ![]() ![]() |
![]() ![]() | |
nequal | ![]() ![]() ![]() ![]() |
![]() ![]() ![]() |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |