  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.
