YES TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) lt(x,0()) -> false() lt(0(),s(y)) -> true() lt(s(x),s(y)) -> lt(x,y) if(true(),x,y) -> x if(false(),x,y) -> y div(x,0()) -> 0() div(0(),y) -> 0() div(s(x),s(y)) -> if(lt(x,y),0(),s(div(-(x,y),s(y)))) max/plus interpretations on N: -_A(x1,x2) = max{1, x1, -11} -#_A(x1,x2) = max{29, 28 + x1, 43} 0_A = 13 0#_A = 24 s_A(x1) = max{22, 7 + x1} s#_A(x1) = max{0, 2 + x1} lt_A(x1,x2) = max{14, 1, -1} lt#_A(x1,x2) = max{27, 26 + x1, 43} false_A = 2 false#_A = 23 true_A = 2 true#_A = 1 if_A(x1,x2,x3) = max{21, 7 + x1, 8 + x2, x3} if#_A(x1,x2,x3) = max{29, 29, 0, 7 + x3} div_A(x1,x2) = max{20, 12 + x1, 8} div#_A(x1,x2) = max{23, 21 + x1, 25} precedence: div > - = s = if > 0 > true > lt > false