The identity of the variables in t∈
TΣ(Q∗(X)) doesn’t play a role. It is (implicitely)
assumed, that they are all different. As the function will be used on the
right-hand sides of the rules of linear transducers, the
assumption is justified.
In [DLS02], we have a
more straightforward exit condition: the loop stops, if the transducer
indeed calculate a fixpoint, but this would be much less efficient. We
need to think about the soundness of this exit condition here, though.