Solution (source code)

= Solution

Use the following <context-free grammar>, with start symbol $S$:
$$
\boxed{S\longrightarrow\epsilon\mid S0\mid S1B0,\qquad B\longrightarrow\epsilon\mid B1B0.}
$$
The symbol $B$ generates the balanced members of the <suffix-nonnegative binary language>, while $S$ permits extra zeros. To prove the claim and prepare the ambiguity argument, reverse every generated <string>. The reversed productions are
$$
U\longrightarrow\epsilon\mid0U\mid0D1U,\qquad D\longrightarrow\epsilon\mid0D1D.
$$
Here $U$ represents the reversals of the $S$ <strings>, and $D$ represents the reversals of the $B$ <strings>. A <string> belongs to the desired <formal language> precisely when its reversal has no <string prefix> with more ones than zeros. Associate a path with each reversed <string>, counting a zero as a step $+1$ and a one as a step $-1$.

The nonterminal $D$ generates exactly the paths that stay nonnegative and finish at zero. The production $0D1D$ consists of an initial up-step, a balanced path one level higher, a down-step to zero, and another balanced path. Conversely, any nonempty balanced nonnegative path has a first return to zero, and splitting there gives exactly this form. <Mathematical induction> on length proves the characterization.

The productions for $U$ generate nonnegative paths: $0U$ stays strictly above zero after its first step, while $0D1U$ first executes a balanced excursion and then another nonnegative path. Conversely, a nonempty nonnegative path starts with zero. If it never returns to height zero, removing that initial zero leaves a nonnegative path, giving $0U$. If it does return, split at its first return to obtain $0D1U$. These shorter components can be generated by <mathematical induction>. This proves that the original <context-free grammar> generates exactly the required <formal language>.

For instance, in the original <context-free grammar>,
$$
S\Rightarrow S1B0\Rightarrow S01B0\Rightarrow01B0\Rightarrow01B1B00\Rightarrow011B00\Rightarrow01100,
$$
while $S\Rightarrow S1B0\Rightarrow S1B01B0\Rightarrow^*1010$. The <string> $110$ is excluded since its entire length is a <string suffix> having two ones and only one zero.