Solution (source code)

= Solution

An accepting derivation in a right-linear grammar has the form
$$
S\Rightarrow w_1A_1\Rightarrow
w_1w_2A_2\Rightarrow\cdots
\Rightarrow w_1\cdots w_m,
$$
with one active variable until the final terminal production.

If no variable repeated on any accepting derivation, an accepting derivation could contain at most $|V|$ variable occurrences. Since the production set is finite, only finitely many such derivations and hence finitely many terminal words would exist. The hypothesis that $\mathcal L(G)$ is infinite therefore supplies an accepting derivation in which some variable $A$ occurs twice.

Split this derivation at the two occurrences:
$$
S\Rightarrow^*uA,\qquad
A\Rightarrow^*vA,\qquad
A\Rightarrow^*z,
$$
where $u,v,z\in\Sigma^*$. The first segment makes $A$ an <accessible variable of a regular grammar>, the middle segment makes it a <looping variable of a regular grammar>, and the last makes it a <terminable variable of a regular grammar>. Thus $A$ has all three properties, proving the <accessible looping terminable variable criterion>.