As shown in [1]}, if \(\tau _2\)  is accepted by \(A_2\) , then an accepting run of \(A_2\)  on \(\tau _2\)  yields a tree \(\tau \)  where the \(\Sigma _\mathcal {O}\)  labeling depends only on the \(\Sigma _\mathcal {B}\)  labeling. In particular, if \(\mathcal {A}_2\)  is nonempty, it is witnessed by a finite-state transducer \(T_2\) . We thus have to check that \(\mathcal {A}_2\)  is nonempty. For this we use standard techniques in tree-automata theory [2]}, according to which nonemptiness of \(\mathcal {A}_2\)  can be checked in exponential time. A subtle point here is that the transition function of \(\mathcal {A}_2\)  is of exponential size, due to the disjunction \(\bigvee _{\eta :\Sigma _\mathcal {I}\rightarrow (\Sigma _\mathcal {B}\times \Sigma _\mathcal {O})}\) . But in the nonemptiness algorithm this disjunction of exponential size turns into an alphabet of exponential size, and this affects the computational complexity multiplicatively, so the algorithm is still exponential with respect to \(\mathcal {A}_R\) .
