Let $\uparrow$ denote the right-associative exponentiation operator: $a\uparrow b\uparrow c=a\uparrow(b\uparrow c)=a^{b^c}$
There is a sequence $A248907$ recently submitted to OEIS (see also $A256179$):
$2, 3, 22, 23, 32, 222, 33, 322, 223, 232, 323, 332, 2222, 3222, 233, 333, 2322, ...$
It represents all power towers of numbers $2$ and $3$ in increasing order. In other words, it consists of all non-empty finite strings over the alphabet $\{2,3\}$ ordered in such a way, that once each string of digits is interspersed with the $\uparrow$ operators and evaluated, the sequence of results is monotonically increasing, i.e.
$2=2$
$3=3$
$2\uparrow2=4$
$2\uparrow3=8$
$3\uparrow2=9$
$2\uparrow2\uparrow2=16$
$3\uparrow3=27$
$3\uparrow2\uparrow2=81$
$...$
I'm interested in a reasonably efficient algorithm for generating $n^\text{th}$ element of $A248907$ (denote it $a_n$). It should avoid direct evaluation of power towers, otherwise it would easily run into huge numbers that would make the algorithm unfeasible in practice.
I have a recursive algorithm that I suppose does the right thing, but I lack a rigorous proof of that.
- If $n\le12$, the corresponding elements $a_1\,..\,a_{12}$ are $2, 3, 22, 23, 32, 222, 33, 322, 223, 232, 323, 332;$
- Otherwise, if $n$ is odd, $a_n$ is $a_{(n-1)/2}$ with the digit $2$ prepended to it;
- Otherwise ($n$ is even), $a_n$ is $a_{(n-2)/2}$ with the digit $3$ prepended to it.
This algorithm builds the sequence from an "irregular" initial segment, and a "regular" tail consisting of pairs of elements that differ by the first digit ($2$ or $3$, interleaved) that is prepended to previous elements taken sequentially from a certain offset, each element is used twice.
Could you please help me prove (or disprove) its correctness?