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