YES TRS: half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) s(log(0())) -> s(0()) log(s(x)) -> s(log(half(s(x)))) max/plus interpretations on N: half_A(x1) = max{1, -7 + x1} half#_A(x1) = max{1, -1} 0_A = 1 0#_A = 3 s_A(x1) = max{9, 7 + x1} s#_A(x1) = max{2, 3} log_A(x1) = max{3, 1 + x1} log#_A(x1) = max{0, -3 + x1} precedence: s > log > half > 0