Теорема Иммермана
| Определение: | 
| Задача несуществования пути между двумя заданными вершинами в данном графе в графе G нет пути из s в t | 
| Теорема: | 
| Доказательство: | 
| 
 Очевидно, что язык является дополнением языка . Чтобы показать, что , придумаем недетерминированный алгоритм, использующий дополнительной памяти, который проверяет, достижима ли вершина из . Определим = { существует путь из в длиной }. Другими словами это множество всех вершин, достижимых из не более чем за шагов. Введем обозначение . Если , где , то не существует путь из в в графе , то есть . Можно построить недетерминированный алгоритм, который будет решать задачу на памяти (это будет доказано ниже). Таким образом показано, что . Поскольку , то аналогичным образом . Получаем, что любую задачу из можно свести к задаче из , а значит . Из соображений симметрии , а значит . | 
| Лемма: | 
Можно построить недетерминированный алгоритм, который будет решать задачу  на  памяти.  | 
| Доказательство: | 
| 
 Для начала приведем недетерминированный алгоритм, находящий путь между двумя вершинами с длиной не более заданной. CheckPath() for do if reject if reject Теперь можно построить недетерминированный алгоритм, который будет принимать на вход и (в случае корректности ) будет перечислять все вершины из на памяти. Enumerate() //количество уже найденных и выведенных элементов for do //перебираем все вершины графа //недетерминированно угадываем путь из s до v или переходим к следующей вершине if continue CheckPath ++ output //выдаем вершину, до которой угадали путь if //не нашли вершин, не допускаем reject Enumerate перебирает все вершины на логарифмической памяти и пытается угадать путь до этой вершины из . Под угадыванием пути подразумевается последовательность недетерминированных выборов следующей вершины пути из в . Для угадывания пути необходимо памяти, так как необходимо лишь хранить текущую и следующую угадываемую вершины угадываемого пути. Теперь, имея Enumerate, можно по индукции строить . Очевидно, что , так как содержит единственную вершину — . Пусть известно значение . Напишем программу, которая на логарифмической памяти будет находить . 
 Next() // хотя бы один, так как for : do //перебираем все вершины графа, кроме — это кандидаты на попадание в for do //перебираем все ребра, входящие в if in Enumerate() //перечисляем все вершины из , если одна из них, то ++ //увеличиваем количество найденных вершин и переходим к рассмотрению следующего кандидата break return 
 Теперь напишем алгоритм, который будет недетерминированно решать задачу на логарифмической памяти. Он будет состоять из двух частей: вычисление и перечисление всех вершин из . Вычисление происходит путем вызова Next раз, при этом каждый раз в качестве подставляется новое полученное значение. 
 NCONN() // for do //вычисляем Next() if in Enumerate() //перечисляем вершины из , если была перечислена, то достижима и выдаем reject, иначе accept reject else acceptДанный алгоритм использует памяти, так как для хранения и необходимо , и для вызываемых Next и Enumerate необходимо памяти.  |