Аннотация:Мы формулируем системы преобразований термов, число шагов работы которых на произвольном входе конечно, но не ограничивается никакой вычислимой функцией, доказуемо тотальной в арифметике Пеано PA. Тем самым, утверждение о сходимости таких систем не доказуемо в PA. Эти системы получаются из независимого комбинаторного утверждения, известного как принцип Червя; их также можно рассматривать как вариант хорошо известной игры Геракла и Гидры, введённой Дж.Парисом и Л.Кирби.