一句话：提出星游戏，用树上的简单规则直接证明重写终止性，并给出 Hydra 战斗的无序数证明。
递归路径序是项重写中证明终止性的关键工具。本文重新表述递归路径序：在树或项上引入星号控制符号，表示将被定义的序中该树变小的命令，由此得到星游戏。星游戏为许多重写任务的终止性证明提供了方便框架。作者表明，即使在有限无标号树上使用最简单的星游戏，也能直接证明著名 Hydra 战斗的终止性，且无需提及序数。文章还给出建立星游戏的另一条路线，基于 Buchholz 的证明方法（经 van Oostrom 改编），得到星控制符号的定量版本。最后提出若干问题与未来方向。
The recursive path ordering is an established and crucial tool in term rewriting to prove termination. We revisit its presentation by means of some simple rules on trees (or corresponding terms) equipped with a 'star' as control symbol, signifying a command to make that tree (or term) smaller in the order being defined. This leads to star games that are very convenient for proving termination of many rewriting tasks. For instance, using already the simplest star game on finite unlabeled trees, we obtain a very direct proof of termination of the famous Hydra battle, direct in the sense that there is not the usual mention of ordinals. We also include an alternative road to setting up the star games, using a proof method of Buchholz, adapted by van Oostrom, resulting in a quantitative version of the star as control symbol. We conclude with a number of questions and future research directions.