# Greibach Normal Form: Proof every sentential form is of the form xy with x terminals and y variables

For any grammar in Greibach normal form, every sentential form obtained from S by a partial left-most derivation is of the form xy with x terminals and y variables.

I think that this can be proven inductively based on the length of the derivation.

Base case: length 1

S -> a with 'a' being a terminal. This follows from the definition of Greibach Normal Form.

Induction step: Let's assume that it is true for all derivations of length n, and imagine I have a derivation of length n + 1.

S =>* xABC... => xadBC... if A -> ad with 'a' being a terminal and d being some variables. Since a grammar in Greibach Normal Form only contains variables to the right of a single terminal symbol, this induction step is also proven and so xa are terminals and dBC... are variables.

I'm not sure about my reasoning and wanted to ask if someone could correct/finish my proof?

Actually we can start with derivations of length 0 as our base case. Obviously we now only have $$S \Rightarrow_\ell^0 S$$, and $$S$$ is of the proper form (to be pedantic: with $$S=xy$$ where $$x=\varepsilon$$ consisting of terminals and $$y=S$$ consisting of variables).
Given a leftmost derivation in $$n+1$$ steps $$S \Rightarrow_\ell^{n+1} \alpha$$ we apply inductive hypothesis on the first $$n$$ steps and have $$S \Rightarrow_\ell^n xAy \Rightarrow_\ell \alpha$$, where $$x$$ consists of terminals, $$y$$ consists of non-terminals, and $$A$$ is (the leftmost) nonterminal. Productions in GNF are of the from $$A\to a v$$ with terminal $$a$$ and a string of nonterminal variables $$v$$ (that might be empty). If we apply such a production to $$A$$ in the last step of the above derivation we get $$\alpha = xavy$$. This is of the proper form $$\alpha = x'y'$$ with $$x'= xa$$ consisting of terminals and $$y'= vy$$ consisting of variables. Done.