YES TRS: a(b(x)) -> b(a(x)) a(c(x)) -> x max/plus interpretations on N: a_A(x1) = max{2, 1 + x1} a#_A(x1) = max{2, 3} b_A(x1) = max{4, 2 + x1} b#_A(x1) = max{0, 1} c_A(x1) = max{0, -1 + x1} c#_A(x1) = max{0, x1} precedence: a = c > b