Crucially though, by Lemma 11 we know that as long as we are interested only in transformed derivations it is sufficient to use a finite number of rule instances-more specifically those whose input and output categories are included in the set K of arity-bounded categories.
for every instance X/Y Yβ Xβ where all three categories are in K, we construct a production and similarly for backward rules.