the same state starting from the initial state. Hence, first part of lemma is true. The second part is proved by contradiction. Let's suppose there are p+1 times i1,...,ip+1 such that no two of them are equivalent. For l > max(i1,...,ip+1), we would have, for each m and n, not E(im,in,l). Therefore there would be p+1 equivalence classes, as judged at l, contradicting the first part of the lemma. Lemma 2 w ∈ αβω if and only if there exists a time i such that there are infinitely many times equivalent to i and favoring i. Proof: Let's suppose w ∈ αβω then there exists a strictly increasing sequence of times i0,i1,i2,... such that w(0,i0) ∈ α and w(in,in+1) ∈ β. Therefore, for all n > m, w(im,in) ∈ β* and in favors im. So, all the i's are members of one of the finitely many equivalence classes (shown in Lemma 1). So, there must be an infinite subset of all i's that belongs to same class. The smallest member of this subset satisfies the right hand side of this lemma. Conversely, suppose in w, there are infinitely many times that are equivalent to i and favoring i. From those times, we will construct a strictly increasing and infinite sequence of times i0,i1,i2,... such that w(0,i0) ∈ αβ* and w(in,in+1) ∈ β*. Therefore w would be in αβω. We define this sequence by induction: Base case: w(0,i) ∈ αβ* because i is in a equivalence class. So, we set i0=i. We set i1 such that i1 favors i0 and E(i0,i1). So, w(i0,i1) ∈ β*. Induction step: Suppose E(i0,in). So, there exists a time i' such that E(i0,in,i'). We set in+1 such that in+1 > i', in+1 favors i0, and E(i0,in+1). So, w(i0,in+1) ∈ β* and, since in+1 > i' we have by definition of E(i0,in,i'), w(in,in+1) ∈ β*. Muller automaton construction We have used both the concepts of "favor" and "equivalence" in Lemma 2. Now, we are going to use the lemma to construct a Muller automaton for language αβω. 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. The machine below is described informally. Note that this machine will be a deterministic Muller automaton. The machine contains p+2 deterministic finite automaton and a master controller, where p is the size of