A simple successor rule gives a Hamiltonian cycle in Knuth's shift-and-save-or-bump digraph SB(m, 3) for every m > 1

Knuth's draft of section 7.2.2.4 of The Art of Computer Programming defines the digraph $SB(m, 3)$, whose vertices are the strings $xyz$ over $\{0, \dots, m-1\}$ and whose arcs go from to ("save") and to ("bump"), and poses exercise , rated as a research problem: construct a Hamiltonian cycle in for all . We give a successor rule whose choice between save and bump at depends only on , and , through comparisons with , , , and , and prove with the Lean proof assistant that for every its walk from visits all vertices and returns to after exactly steps. The proof follows the walk's first returns to the vertices , which have closed forms region by region, and checks the small cases by computation in the kernel. This answers the exercise for every .