YES TRS: norm(nil()) -> 0() norm(g(x,y)) -> s(norm(x)) f(x,nil()) -> g(nil(),x) f(x,g(y,z)) -> g(f(x,y),z) rem(nil(),y) -> nil() rem(g(x,y),0()) -> g(x,y) rem(g(x,y),s(z)) -> rem(x,z) max/plus interpretations on N: norm_A(x1) = max{0, x1} norm#_A(x1) = max{0, x1} nil_A = 0 nil#_A = 0 0_A = 0 0#_A = 0 g_A(x1,x2) = max{0, x1, x2} g#_A(x1,x2) = max{0, x1, x2} s_A(x1) = max{0, x1} s#_A(x1) = max{0, x1} f_A(x1,x2) = max{0, x1, x2} f#_A(x1,x2) = max{0, x1, x2} rem_A(x1,x2) = max{0, x1, x2} rem#_A(x1,x2) = max{0, x1, x2} precedence: nil > 0 = f > g > s = rem > norm