Authors: Johannes Niederhauser ; Nao Hirokawa ; Aart Middeldorp

We revisit completion modulo equational theories for left-linear term rewrite systems where unification modulo the theory is avoided and the normal rewrite relation can be used in order to decide validity questions. To that end, we give a new correctness proof for finite runs and establish a simulation result between the two inference systems known from the literature. Given a concrete reduction order, novel canonicity results show that the resulting complete systems are unique up to the representation of their rules' right-hand sides.
Furthermore, we show how left-linear AC completion can be simulated by general AC completion. In particular, this result allows us to switch from the former to the latter at any point during a completion process.