YES TRS: minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) quot(0(),s(y)) -> 0() quot(s(x),s(y)) -> s(quot(minus(x,y),s(y))) max/plus interpretations on N: minus_A(x1,x2) = max{4, x1, -6} minus#_A(x1,x2) = max{0, 2, 1} 0_A = 10 0#_A = 7 s_A(x1) = max{11, 7 + x1} s#_A(x1) = max{6, 2 + x1} quot_A(x1,x2) = max{7, 3 + x1, 4} quot#_A(x1,x2) = max{3, -2 + x1, 4} precedence: 0 > quot > minus = s