Levi's lemma

[1] Levi's lemma can be applied repeatedly in order to solve word equations; in this context it is sometimes called the Nielsen transformation by analogy with the Nielsen transformation for groups.

This approach results in a graph of substitutions generated by repeatedly applying Levi's lemma.

[2] A more general method for solving word equations is Makanin's algorithm.

[6] A monoid in which Levi's lemma holds is said to have the equidivisibility property.

(Note that f simply being a homomorphism does not guarantee this latter property, as there could be multiple elements of M mapped to 0.