Equational theory of ordinals with addition and left multiplication by $\omega$

Abstract

We show that the equational theory of the structure $⟨{\omega }^{\omega }:(x,y)\mapsto x+y,x\mapsto \omega x⟩$ is finitely axiomatizable and give a simple axiom schema when the domain is the set of transfinite ordinals. We give an algorithm that given a pair of terms $(E,F)$ decides in linear time with respect of their common length whether or not $E=F$ is a consequence of the axioms.