 Accessible looping terminable variable criterion

If a finite right-linear grammar generates an infinite language, some variable is accessible, looping, and terminable. It is the repeated variable on a sufficiently long accepting derivation.