YES TRS: div(X,e()) -> i(X) i(div(X,Y)) -> div(Y,X) div(div(X,Y),Z) -> div(Y,div(i(X),Z)) max/plus interpretations on N: div_A(x1,x2) = max{1, 2 + x1, x2} div#_A(x1,x2) = max{1, 2 + x1, x2} e_A = 3 e#_A = 3 i_A(x1) = max{2, 2 + x1} i#_A(x1) = max{2, 2 + x1} precedence: div = e = i