Proof of Part (2): This is the more complicated part of this proof. Just like in the previous case, we start by writing the formula \(f\)  in Disjunctive Normal Form (DNF). We can then separate each clause into conjunctions of word equation literals and regular language membership literals. By closure properties of regular languages, we can remove negations of regular language membership constraints and by canonical constructions (see e.g. [1]}), we can replace the word equation literals with a single word equation atom (i.e. a positive occurrence of a word equation) without affecting the language expressed by \(x\) . Thus the language expressed by \(x\)  is a finite union of languages, each given by the solutions to a single word equation which adhere to the (positive) regular language membership constraints (and projected onto the variable \(x\) ).
