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)) max/plus interpretations on N: ack_A(x1,x2) = max{8, -4 + x1, x2} ack#_A(x1,x2) = max{1, -11 + x1, -7 + x2} 0_A = 6 0#_A = 0 s_A(x1) = max{3, x1} s#_A(x1) = max{1, -6} precedence: ack > s > 0