On some slowly terminating term rewriting systems

We formulate some term rewriting systems in which the number of computation steps is finite for each output, but this number cannot be bounded by a provably total computable function in Peano arithmetic $\mathsf{PA}$. Thus, the termination of such systems is unprovable in $\mathsf{PA}$. These systems are derived from an independent combinatorial result known as the Worm principle; they can also be viewed as versions of the well-known Hercules-Hydra game introduced by Paris and Kirby.
Bibliography: 16 titles.