How to prove numerical formula about strings in context-free language? Consider the the alphabet $\{0,1\}$ and the grammar $S\to 10,\, S\to 1SS0$. Define $P$ to be the set of all those strings and $P_n$ be the set of all strings in $P$ in which the substring $10$ occur exactly $n$ times. Let $A_n$ be the smallest number in $P_n$ if the binary strings are interpreted as binary numbers.

How to prove that $\displaystyle A_n=2^n\cdot\frac{3\cdot(8^n-1)-7}{14}\:$?

I got the formula from computer simulations and intuition, but how to prove it?
 A: Sketch of a proof.
Let $P$ be the language of $\{0, 1\}^*$ generated by the grammar and let $P_n$ be the set of all words in $P$ in which the factor $10$ occurs exactly $n$ times. Equivalently, $P_n$ is the set of words of $P$ whose derivation tree uses $n$ times the nonterminal symbol $S$. Let $u_n$ be the shortest word of $P_n$ in the lexicographic order. For instance
\begin{align}
S &\to 10 = u_1 \\
S &\to \color{red}{1SS0} \xrightarrow{*} 110100 = u_2 \\
S &\to 1SS0 \to 1S\color{red}{1SS0}0 \xrightarrow{*} 1101101000 = u_3 \\
S &\to 1SS0 \to 1S1SS00 \to 1S1S\color{red}{1SS0}00 \xrightarrow{*} 11011011010000 = u_4 \\
S &\to 1SS0 \to 1S1SS00 \to 1S1S1SS000 \to 1S1S1S\color{red}{1SS0}000 \xrightarrow{*} 110110110110100000 = u_5
\end{align}
where the last steps of the derivation (indicated by $\xrightarrow{*}$) consists
in replacing each occurrence of $S$ by $10$.
Step 1. The derivation of $u_n$ is obtained by using the rule $S \to 1SS0$ on the rightmost $S$ (as emphasized with the red color). Indeed, the words produced by other derivations would come after $u_n$ in the lexicographic order: for instance, $S \to 1SS0 \to 1\color{red}{1SS0}S0 \xrightarrow{*} 1110100100 > u_3$.
Step 2. It follows that $u_n = (110)^{n-1}100^{n-1}$
Step 3. Let $A_n$ be the binary number represented by $u_n$. Then $A_1 = 2$. Moreover, observing that
$$
u_{n+1} = (110)u_n0 \quad \text{and}\quad |u_n| = 4n-2
$$
one gets, since $u_n0$ represents $2A_n$ and $110$ represents $6$
$$
A_{n+1} = 6 \times 2^{|u_n| + 1} + 2A_n = 3 \times 2^{4n-1} + 2A_n
$$
and it is not difficult to verify that 
$$
A_n = 2^{n-1} \bigl(3(1 + 8 + \dotsm + 8^{n-1})-1\bigr)
$$
which is exactly your formula.
