Will this algorithm terminate on any input?
This is my idea for a proof although I am not quite sure whether it works:

Consider $r$, the number of symbols on all right-hand sides and $n$, the number of distinct nonterminals. Each grammar has a specific tuple $(r-n,n)$. Let's define an order on grammars. We first sort by $r-n$ and in case the values are equal by $n$.

Whenever step one fires, $r$ decreases as each rule has at least two symbols on its right hand side. Whenever step two fires, $n$ increases by one and $r$ stays the same (in case only two pairs are found) or decreases (if two or more pairs are found). If the third step fires, $r$ decreases by one and $n$ also decreases by one as one nonterminal is replaced by the whole right hand side of its definition which is removed. Let $G'$ be the tuple of the grammar (whose tuple is $G$) after the application of any of those steps, then:


step 1 always reduces $r-n$ by at least one, $G' &lt; G$
step 2 always reduces $r-n$ by at least one, $G' &lt; G$
step 3 does not change $r-n$ but reduces $n$ by one, $G' &lt; G$


The application of each step reduces the tuple of $G$ to a lower tuple. What is left is to show, that both $r-n$ and $n$ have a lower bound. Per definition $n\ge1$. Since each nonterminal is defined in terms of exactly one rule, $n$ is also the number of rules. Since each rule has at least two symbols on it's right-hand side, $r\ge2n\to r&gt;n\to r-n&gt;0$. The tuples  have a lower bound that is eventually reached. Thus the algorithm must eventually terminate.