О нижней границе временной сложности проблемы разрешимости теории целых чисел с функцией следования и оператором наименьшей фиксированной точки

Мы показываем, что всякий разрешающий алгоритм для теории целых чисел с функцией следования и оператором наименьшей фиксированной точки для формулы с $n$ вложенными операторами имеет временную сложность не меньше гиперэкспоненциальной.
Доказательство происходит в два этапа. На первом этапе мы показываем, как с помощью короткой формулы представить сдвиг на экспоненциальную величину. Для этого мы строим оператор наименьшей фиксированной точки, который в некоторой кодировке последовательно перечисляет двоичные записи начального отрезка натуральных чисел.
На втором этапе мы показываем, как при помощи оператора фиксированной точки и построенной нами формулы моделировать работу клеточного автомата с гиперэкспоненциальной оценкой временной сложности. При этом длина построенной нами формулы линейно зависит от длины входных данных автомата.