}
</div>
Инвариант: после <tex>j</tex> итераций внутреннего цикла для <tex>i</tex>
*для <tex>k < i</tex> правые части правил вывода из <tex>A_k</tex> не начинаются с <tex>A_1, A_2, \ldots , A_k</tex>
*правые части правил вывода из <tex>A_i</tex> не начинаются с <tex>A_1, A_2, \ldots , A_j</tex>
*правые части правил вывода не начинаются с добавленных алгоритмом нетерминалов <tex>A_k ^{\prime}</tex>
*грамматика не содержит ε-правил
(проверяется индукцией по парам <tex>(i,j)</tex>)
Таким образом, после применения алгоритма все правила вывода имеют вид
