[1] This theorem is proven by supplying an algorithm to construct a deterministic Muller automaton for any ω-regular language and vice versa.
In McNaughton's original paper, the theorem was stated as: "An ω-event is regular if and only if it is finite-state.
Following McNaughton's definition, an ω-event is a finite-state event if there exists a deterministic Muller automaton that recognizes it.
One direction of the theorem can be proven by showing that any given Muller automaton recognizes an ω-regular language.
For 1≤i≤n, let βi be a regular language whose elements take A from qi to q(i mod n)+1 without passing through any state outside of {q1, ... ,qn}.
It is claimed that α(β1 ... βn)ω is the ω-regular language recognized by the Muller automaton A.
Therefore, A accepts the word w. The other direction of the theorem can be proven by showing that there exists a deterministic Muller automaton that recognizes a given ω-regular language.
The union of finitely many deterministic Muller automata can be easily constructed; therefore without loss of generality we assume that the given ω-regular language is of the form αβω.
The proposed automaton will accept a word if and only if a time i exists such that it will satisfy the right hand side of Lemma 2.
If master sets a Aβ* machine to be dormant then it remains in its initial state and oblivious to the input.
Let νn be the set of states in which the red light does not flash corresponding to nth Aβ* machine.