YES TRS: app(id(),x) -> x app(plus(),0()) -> id() app(app(plus(),app(s(),x)),y) -> app(s(),app(app(plus(),x),y)) linear polynomial interpretations on N: app_A(x1,x2) = x1 + x2 + 2 app#_A(x1,x2) = x1 + x2 + 2 id_A = 0 id#_A = 0 plus_A = 1 plus#_A = 1 0_A = 1 0#_A = 1 s_A = 0 s#_A = 0 precedence: app > plus = 0 > id = s