Every proof I can find of this result is by way of regular expressions. Is there any constructive proof that defines the corresponding DFA (probably NFA)? For instance the proof of concatenation closure is most often presented by demonstrating the NFA. I'm just curious whether this is out there somewhere
Does there exist a proof of closure of regular languages under regular substitution by giving the corresponding DFA?
formal languages;reference request;finite automata;closure properties
A full specification of the construction of a finite automaton for regular substitution is given by Algorithm 4.2.7 of [1] (with a several-page proof of correctness). Tedious indeed![1] Meduna, Alexander. Automata and languages: theory and applications Springer, 2000.