The shuffle coincidence theorem (paper §6): a series is shuffle-finite (a shuffle polynomial in a finite tuple of series closed under the left derivatives) if and only if it is recognised by a shuffle automaton. The "finite implies recognisable" direction extends the witnessing tuple by the series itself and builds the automaton from the closure under left derivatives; the "recognisable implies finite" direction reads off the generator tuple $A.sem (X_i)$, closed under left derivatives by the derivation property.