Solution (source code)

= Solution

Fix the first tape of the <group multiplier automaton> $M_x$ to be $u=a_1\cdots a_m$. Construct its possible runs by <dynamic programming>, one column at a time. A record consists of a state and a flag indicating whether the output tape has ended. At column $i\leq m$, the first symbol is $a_i$ and the second symbol may be any letter of the <alphabet>, or $\#$; after the second tape first uses $\#$ it must continue to use $\#$. At later columns the first symbol is $\#$, and an additional column must have a genuine letter on the second tape. Never add a $(\#,\#)$ column.

Keep one predecessor record and its output symbol for each reachable state-and-flag pair in each layer. Two runs reaching the same record have exactly the same possible future completions, so this merging loses no accepting output. The merged <dead state of a finite automaton> can be discarded. At each layer $i\geq m$, test whether a reached state is accepting; the initial layer is included when $m=0$. Upon success, follow predecessor records backwards and omit padding symbols to recover $v$.

The <automatic structure for a group> supplies a representative in $L$ of $\overline u x$, so an accepted <padded convolution of words> exists and this search terminates. \b[The output is the required representative]:
$$
\boxed{v\in L,\qquad \overline v=\overline u x.}
$$
The search uses only the finite transition table; it does not presuppose a solution to the <word problem for a group>.