YES TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) minus(x,0()) -> x minus(s(x),s(y)) -> minus(x,y) mod(0(),y) -> 0() mod(s(x),0()) -> 0() mod(s(x),s(y)) -> if_mod(le(y,x),s(x),s(y)) if_mod(true(),s(x),s(y)) -> mod(minus(x,y),s(y)) if_mod(false(),s(x),s(y)) -> s(x) max/plus interpretations on N: le_A(x1,x2) = max{5, 1, 18 + x2} le#_A(x1,x2) = max{11, 9, 13} 0_A = 20 0#_A = 25 true_A = 6 true#_A = 14 s_A(x1) = max{8, 22 + x1} s#_A(x1) = max{27, 29} false_A = 18 false#_A = 28 minus_A(x1,x2) = max{11, 4 + x1, -1} minus#_A(x1,x2) = max{0, -6 + x1, 1} mod_A(x1,x2) = max{0, 3 + x1, 19 + x2} mod#_A(x1,x2) = max{10, 4 + x1, 10} if_mod_A(x1,x2,x3) = max{1, 26, x2, 19 + x3} if_mod#_A(x1,x2,x3) = max{9, 8 + x1, -6 + x2, 11} precedence: mod > le = if_mod > s = minus > false > 0 > true