Decreasing proof orders

Interpreting conversions in involutive monoids


We introduce the decreasing proof order. It orders a conversion above another conversion if the latter is obtained by filling any peak in the former by a decreasing diagram. The result is developed in the setting of involutive monoids.