(Paraphrasal of problem 2.48a in Sipser - Introduction to the Theory of Computation, 3rd ed.)
The language $L$ consists of all binary strings with a $1$ somewhere in the middle third of the string, and I'm trying to prove $L$ is context-free by showing that it can be generated by a context-free grammar.
Alphabet $A = \{0,1\}$
$L = \{abc \;|\; (a,c \in A^{*}) \wedge (b \in A^{*}1A^{*}) \wedge (|a|=|c|\geq|b|)\}$
So far, I have $S \rightarrow 0S0\; |\; 1S1 \;|\; 0S1 \;|\; 1S0$
This generates $a$ and $c$ AND ensures that $|a| = |c|$. However, I am trying to come up with a way to definitively insert a $1$ at some point, while ensuring that the grammar cannot somehow push that $1$ into $a$ (the first third) or $c$ (the last third).
(I suppose creating a pushdown automaton would also work, and am open to that, as well. However, I usually tend towards CFGs for that kind of question.)
Any advice, pointers, etc. you could offer me will be greatly appreciated - many thanks!