Your computation is correct, as far as I can say. However, to translate the automaton formula, you don't have to double negate it to get an existential automaton inside. If you drive in the outermost negation, it is still a LO2 formula, and is the one obtained directly from the universal automaton.