YES TRS: ack(0(),y) -> s(y) ack(s(x),0()) -> ack(x,s(0())) ack(s(x),s(y)) -> ack(x,ack(s(x),y)) linear polynomial interpretations on N: ack_A(x1,x2) = 1 ack#_A(x1,x2) = 2 0_A = 1 0#_A = 0 s_A(x1) = 1 s#_A(x1) = 1 precedence: s > 0 > ack