The commutativity problem is decidable for recognisable series over a finite alphabet (paper §4). This is the meta-theorem ($EffectivePrevarietyCommutativityDecidable$) applied to $recPrevariety$, the effective prevariety of recognisable series: its boolean decider on a presentation $r$ decides $IsCommutative (recPrevariety.sem r)$, and since $recPrevariety.sem r = r.sem$, it decides $IsCommutative (r.sem)$.