arXiv++ Combinatorics

Let $H$ be an HD0L-system. We show that there are only finitely many primitive words $v$ with the property that $v^k$, for all integers $k$, is an element of the factorial language of $H$. In particular, this result applies to the set of all factors of a morphic word. We provide a formalized proof in the proof assistant Isabelle/HOL as part of the Combinatorics on Words Formalized project.