YES TRS: app(app(plus(),0()),y) -> y app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) app(app(app(curry(),f),x),y) -> app(app(f,x),y) add() -> app(curry(),plus()) max/plus interpretations on N: app_A(x1,x2) = max{0, 3 + x1, x2} app#_A(x1,x2) = max{0, 3 + x1, x2} plus_A = 1 plus#_A = 1 0_A = 0 0#_A = 0 s_A = 2 s#_A = 2 curry_A = 0 curry#_A = 0 add_A = 4 add#_A = 4 precedence: add > app = 0 = curry > s > plus