YES 1 decompositions #0 ----------- 1: max(x,0()) -> x 2: max(s(x),s(y)) -> s(max(x,y)) 3: max(x,y) -> max(y,x) @Jouannaud and Kirchner's criterion --- R 1: max(x,0()) -> x 2: max(s(x),s(y)) -> s(max(x,y)) 3: max(x,y) -> max(y,x) --- S 1: max(x,0()) -> x 2: max(s(x),s(y)) -> s(max(x,y)) 3: max(x,y) -> max(y,x)