Accessible looping terminable variable criterion
= 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.