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