Here we prove the following theorem.

Theorem. For every deterministic Muller automaton, there is an equivalent deterministic parity automaton.

 

The above theorem can be proved in two ways. One of them is to show that, by taking more care, we can actually produce a parity automaton in the determinisation construction. Here we use an alternative construction, based on a data structure called the latest appearance record that was found by McNaughton. The construction is presented in the following lemma.

Lemma. For every finite alphabet , there exists a deterministic automaton with input alphabet , a totally ordered state space , and a function 

   

with the following property. For every input word, the set of letters appearing infinitely often in the input is obtained by applying to the smallest state that appears infinitely often in the run.

Proof. The state space consists of pairs

   

such that is a non-repeating word, i.e. it contains each letter at most once. The initial state of the automaton is . After reading a finite input word, the state of the automaton is:
• The word obtained from the input by keeping only the latest appearance of each letter (call this the latest appearance record).
• The length of the longest common prefix of the latest appearance records in the current and previous states (call this the hit position).

It is not difficult to define the transition function of the automaton to make the above invariant true. Here is an example run:

   

The key observation is this: if is the smallest hit position that appears infinitely often, then there are exactly letters in the input word that appear at least once but finitely often. In particular, if the smallest state that appears infinitely often is then by removing the first letters of we get the set of letters that appear infinitely often in the input word.  (To be fully precise, there is an exception: if , then the set of letters that appears infinitely often is the last letter in .)

Therefore, to get the statement of the lemma, we order first by hit positions, and in case of equal hit positions we use some arbitrary total ordering on the latest appearance records. The function is defined according to the description in the previous paragraph. 

The conversion of Muller to parity is a straightforward corollary of the above lemma: one applies the above lemma to the state space of the Muller automaton, and defines the ranks according to the Muller condition.