Matsumoto theorem

Matsumoto's theorem says that any two reduced expressions for one element of a Coxeter group are connected by a finite sequence of braid moves.

Every word in simple Coxeter generators can be reduced by braid moves and cancellations $ss\mapsto 1$. Consequently, a word is reduced exactly when no sequence of braid moves can make a cancellation possible.