YES TRS: half(0()) -> 0() half(s(0())) -> 0() half(s(s(x))) -> s(half(x)) bits(0()) -> 0() bits(s(x)) -> s(bits(half(s(x)))) max/plus interpretations on N: half_A(x1) = max{8, -5 + x1} half#_A(x1) = max{12, -2 + x1} 0_A = 3 0#_A = 5 s_A(x1) = max{13, 5 + x1} s#_A(x1) = max{12, 1 + x1} bits_A(x1) = max{2, 1 + x1} bits#_A(x1) = max{0, -1 + x1} precedence: bits > half > s > 0