It was proven independently by Neil Immerman and Róbert Szelepcsényi in 1987, for which they shared the 1995 Gödel Prize.
In its general form the theorem states that NSPACE(s(n)) = co-NSPACE(s(n)) for any function s(n) ≥ log n. The result is equivalently stated as NL = co-NL; although this is the special case when s(n) = log n, it implies the general theorem by a standard padding argument.
No similar result is known for the time complexity classes, and indeed it is conjectured that NP is not equal to co-NP.
It has also been used to prove other theorems in computational complexity, including the closure of LOGCFL under complementation and the existence of error-free randomized logspace algorithms for USTCON.
However, this algorithm uses too much space to solve the problem in NL, since storing a set Rk requires one bit per vertex.
A mechanism is needed to make all of these branches abort (reject immediately), except the one where all the guesses were correct.
The following pseudocode summarizes the algorithm: As a corollary, in the same article, Immerman proved that, using descriptive complexity's equality between NL and FO(Transitive Closure), the logarithmic hierarchy, i.e. the languages decided by an alternating Turing machine in logarithmic space with a bounded number of alternations, is the same class as NL.