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

one constructs an automaton with:

- subsets of as states,
- as the initial state,
- as accepting states, those for which ,
- for any , the inverse image along as the transition function at .

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

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 there exists a computable function such that, in the automaton obtained from by a Brzozowski phase, every reachable state with support of size is reachable by a word with support of size at most .

The function should be computable for any , and, as a mathematical object, it should also be computable *from* .

My guess is that , where depends only on and not on .

**PRIZE!** I offer a bottle of nice Barbadian rum to the first person who will prove or disprove this conjecture.

**Edit [April 8, 2014]: **The conjecture has been now disproved by Mikołaj Bojańczyk, who gets the bottle. Thanks Mikołaj!