I came across generalized nondeterministic finite automata (GNFAs) in Sipser's Introduction to the Theory of Computation. These are automata where transitions are labelled with regular expressions, rather than single symbols from the alphabet. I thought he would explain why GNFAs are allowed. I mean, an appropriate explanation would be that GNFAs are equivalent to NFAs, or GNFAs are equivalent to DFAs or some such argument. But I couldn't find any such explanation in the book.
Online, I read in this article that you can convert a GNFA to an NFA as follows:
For each transition arrow in the GNFA, we insert the complete automaton accepting the language generated by the transition arrow’s label as a “subautomaton;” this way, we can replace each regular expression by a set of states and character transitions
How is the automaton inserted?
Let's say we have a GNFA with an arrow going from state A to state B labelled with a regular expression R. To convert this GNFA to an NFA, do we get rid of that arrow, instead, take NFA N that recognizes L(R), and create an arrow from A to the start state of N labelled with the epsilon symbol, then create arrows from the accept states of N to B, each also labelled with the epsilon symbol?
Of course the accept states of N would no longer be accept states in the new machine, would they?
I know that GNFAs are equivalent to NFAs but I need a convincing proof, not just a short paragraph mentioning their equivalence.