The equality (zeroness) problem is decidable for shuffle automata over a finite alphabet (paper §6). As in the Hadamard case, the orbit-ideal chain $I_n$ stabilises by Hilbert's basis theorem ($orbitIdeal_stabilises$), and the stabilised ideal is a bi-ideal, so the zeroness of the recognised series is characterised by the finite statement $∀ p ∈ orbitSet A N, p ∈ K A$ ($zeroness_iff_orbitSet$). The only difference from the Hadamard case is the transition invariance ($orbitIdeal_image$): the letter map is a derivation (ℚ-linear, not a ring hom), so instead of $Ideal.map_span$ one decomposes $p$ as a finite $R$-linear combination of orbit-set elements and applies the Leibniz rule termwise. The kernel $K A$ is finitely generated ($gensKer$, by Noetherianity), so this finite statement is a batch of ideal-membership queries $p ∈ span ↑(gensKer A)$, each decided by $IdealMembershipDecidable$; the decision $d$ is the Boolean "and" of these queries over the (finite) orbit set.