not flash corresponding to nth Aβ* machine. Let νn be the set of states in which the red light does not flash corresponding to nth Aβ* machine. So, Muller acceptance condition F = { S | ∃n μn ⊆ S ⊆ νn }. This finishes the construction of the desired Muller automaton. Q.E.D. Other proofs Since McNaughton's proof, many other proofs have been proposed. The following are some of them. ω-regular languages can be shown equiv-expressive to Büchi automata. Büchi automata can be shown to equiv-expressive to semi-deterministic Büchi automata. Semi-deterministic Büchi automata can be shown to be equiv-expressive to deterministic Muller automata. This proof follows the same lines as the above proof. Safra's construction transforms a non-deterministic Büchi automaton to a deterministic Rabin automaton. This construction is known to be optimal. There is a purely algebraic proof of McNaughton's theorem. Reference list Automata (computation)