О применении конечных автоматов к исследованию разрешимости теории с оператором фиксированной точки

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