YES Problem: max(x,0()) -> x max(s(x),s(y)) -> s(max(x,y)) max(x,y) -> max(y,x) Proof: AT confluence processor Complete TRS T' of input TRS: max(x,0()) -> x max(s(x),s(y)) -> s(max(x,y)) max(0(),x) -> x max(x,y) -> max(y,x) T' = (P union S) with TRS P:max(x,y) -> max(y,x) TRS S:max(x,0()) -> x max(s(x),s(y)) -> s(max(x,y)) max(0(),x) -> x S is linear and P is reversible. CP(S,S) = 0() = 0() CP(S,P union P^-1) = x = max(0(),x), y = max(0(),y), s(max(x156,x157)) = max(s(x157),s(x156)), s(max(x158,x159)) = max(s(x159),s(x158)), y = max(y,0()), x = max(x,0()) CP(P union P^-1,S) = max(0(),x) = x, max(s(y),s(x)) = s(max(x,y)), max(x,0()) = x We have to check termination of S: Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = 3x0 + 2, [max](x0, x1) = 5x0 + x1 + 5, [0] = 0 orientation: max(x,0()) = 5x + 5 >= x = x max(s(x),s(y)) = 15x + 3y + 17 >= 15x + 3y + 17 = s(max(x,y)) max(0(),x) = x + 5 >= x = x problem: max(s(x),s(y)) -> s(max(x,y)) Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = 4x0 + 4, [max](x0, x1) = x0 + x1 + 1 orientation: max(s(x),s(y)) = 4x + 4y + 9 >= 4x + 4y + 8 = s(max(x,y)) problem: Qed