Детерминизация ординальных автоматов

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