YES TRS: app(app(apply(),f),x) -> app(f,x) max/plus interpretations on N: app_A(x1,x2) = max{3, 2 + x1, 3 + x2} app#_A(x1,x2) = max{0, -2, -1} apply_A = 1 apply#_A = 0 precedence: app = apply