for}
     &{\mbox{\sc top}}(x_1) \doteq A_0 \wedge   \\
    &&{\mbox{\sc top rest}}(x_1) \doteq A_1 \wedge  \\
    &&{\centering \vdots}\\
    &&{\mbox{\sc top rest}}^n(x_1) \doteq A_n \wedge\\
    &&{\mbox{\sc rest}}^{n+1}(x_1) \doteq x_0   \\
{\mbox{\sc pop}}(A) &\mbox{stands for}
     &{\mbox{\sc top}}(x_0) \doteq A \wedge \\
    &&{\mbox{\sc rest}}(x_0) \doteq x_1 \\
{\mbox{\sc empty-stack}}    &\mbox{stands for}  &x_0 \doteq \$\end{aligned}$$

We have to prove that GNF $G$ and its simulation by R-AVG $G'$ generate (almost) the same language. Obviously, R-AVG $G'$ cannot generate the empty string. However, for all non-empty strings the following theorem holds.

Start nonterminal $S$ of GNF $G$ derives string $\alpha$ ($\alpha \in \Sigma^+$) if, and only if, start nonterminal $S$ of R-AVG $G'$ derives string $\alpha$ with the empty stack.

There are two cases to consider. First, $S$ derives string $\alpha$ in one step. Second, $S$ derives string $\alpha$ in more than one step. The lemma below is needed in the proof of the second case.

Case I

:   Let start nonterminal $S$ derive string $\alpha$ in one step. GNF $G$ contains a production $S \rightarrow \alpha$ iff R-AVG $G'$ contains a production $S \rightarrow \alpha$ with the equation . So, $S$ derives $\alpha$ in a derivation of GNF $G$ iff $S$ derives $\alpha$ with an empty 