YES TRS: le(0(),y) -> true() le(s(x),0()) -> false() le(s(x),s(y)) -> le(x,y) pred(s(x)) -> x minus(x,0()) -> x minus(x,s(y)) -> pred(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{2, 1, 1} le#_A(x1,x2) = max{6, 14, 7} 0_A = 10 0#_A = 2 true_A = 2 true#_A = 1 s_A(x1) = max{0, 6 + x1} s#_A(x1) = max{0, 3} false_A = 2 false#_A = 1 pred_A(x1) = max{4, -2 + x1} pred#_A(x1) = max{0, 2} minus_A(x1,x2) = max{4, 1 + x1, 3} minus#_A(x1,x2) = max{2, 2, 3} mod_A(x1,x2) = max{10, 3 + x1, 4} mod#_A(x1,x2) = max{5, 8 + x1, -1} if_mod_A(x1,x2,x3) = max{10, 6, x2, 4} if_mod#_A(x1,x2,x3) = max{13, 4, 4 + x2, 6} precedence: mod > le = 0 = if_mod > true = false = minus > s = pred