HD0L-系统语言中无界指数本原词的数量是有限的
The number of primitive words of unbounded exponent in the language of an HD0L-system is finite
AI总结：
本文证明 HD0L-系统语言中满足任意整数次幂都属于其因子语言的本原词仅有有限多个，并在 Isabelle/HOL 中完成了形式化验证。
摘要：
设 $H$ 为一个 HD0L-系统。我们证明，只有有限多个本原词 $v$ 具有如下性质：对于所有整数 $k$，$v^k$ 都是 $H$ 的因子语言中的元素。特别地，这一结果适用于一个态射词的所有因子构成的集合。我们在证明助手 Isabelle/HOL 中提供了形式化证明，作为 Combinatorics on Words Formalized 项目的一部分。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
