This gives a proof of correctness of the algorithm at node_string.rs. Unless otherwise specified, lowercase letters are used for variables for single symbols and group generators, and uppercase letters are used for variables for strings and group elements. 1 is the empty string or the identity element of a group. X$Y means every symbol of A commutes with every symbol of B (as group generators).
Let G be a right-angled coxeter group over the set of generators S. This just means that G is a group presented by aa = 1 for each a in S and any set of equations of the form ab = ba (or equivalently abab = 1) for a ≠ b. In addition, there is a linear order < over S.
The algorithm rewrites strings of the form Xa into a canonical form, assuming X is already in