A conjecture concerning Brzozowski algorithm (PRIZE!)

Fix attention on equality atoms.

Given an orbit-finite, deterministic automaton on the alphabet of atoms, a Brzozowski phase amounts to:

reversing the direction of all transition arrows and swapping initial and accepting states,
determinising the result, and
cutting to the reachable part.

In other words, given an automaton

$A = \langle Q,q_0,F,(\stackrel{a}{\to})_{a\in\mathbb{A}}\rangle$

one constructs an automaton with:

subsets of $Q$ as states,
$F$ as the initial state,
as accepting states, those $P\subseteq Q$ for which $q_0\in P$ ,
for any $a\in\mathbb{A}$ , the inverse image along $\stackrel{a}{\to}$ as the transition function at $a$ .

The result of this may be orbit-infinite even after restricting to the reachable part; for example, consider as $A$ the minimal automaton for the language

$L = \{a_1\cdots a_n\mid \exists i<n.\ a_i=a_n\}.$

However, the resulting automaton is always locally finite: any fixed finite set of atoms supports only finitely many states.

I conjecture that, moreover, any reachable state with a small support can be reached by a word with a small support. More formally:

Conjecture. For any automaton $A$ there exists a computable function $f:\mathbb{N}\to\mathbb{N}$ such that, in the automaton obtained from $A$ by a Brzozowski phase, every reachable state with support of size $n$ is reachable by a word with support of size at most $f(n)$ .