YES Problem: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) s(p(x)) -> x p(s(x)) -> x +(x,y) -> +(y,x) Proof: AT confluence processor Complete TRS T' of input TRS: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) s(p(x)) -> x p(s(x)) -> x +(x,y) -> +(y,x) T' = (P union S) with TRS P:+(x,y) -> +(y,x) TRS S:+(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) s(p(x)) -> x p(s(x)) -> x S is left-linear and P is reversible. CP(S,S) = 0() = 0(), s(x) = s(+(x,0())), p(x) = p(+(x,0())), s(+(0(),x502)) = s(x502), s(+(s(x),x504)) = s(+(x,s(x504))), s(+(p(x),x506)) = p(+(x,s(x506))), p(+(0(),x508)) = p(x508), p(+(s(x),x510)) = s(+(x,p(x510))), p(+(p(x),x512)) = p(+(x,p(x512))), s(y) = s(+(0(),y)), p(y) = p(+(0(),y)), s(+(x516,0())) = s(x516), s(+(x518,s(y))) = s(+(s(x518),y)), s(+(x520,p(y))) = p(+(s(x520),y)), p(+(x522,0())) = p(x522), p(+(x524,s(y))) = s(+(p(x524),y)), p(+(x526,p(y))) = p(+(p(x526),y)), +(x,x528) = s(+(x,p(x528))), +(x529,y) = s(+(p(x529),y)), p(x530) = p(x530), +(x,x531) = p(+(x,s(x531))), +(x532,y) = p(+(s(x532),y)), s(x533) = s(x533) CP(S,P union P^-1) = x = +(0(),x), y = +(0(),y), s(+(x,x561)) = +(s(x561),x), s(+(y,x563)) = +(s(x563),y), p(+(x,x565)) = +(p(x565),x), p(+(y,x567)) = +(p(x567),y), y = +(y,0()), x = +(x,0()), s(+(x570,y)) = +(y,s(x570)), s(+(x572,x)) = +(x,s(x572)), p(+(x574,y)) = +(y,p(x574)), p(+(x576,x)) = +(x,p(x576)) PCP_in(P union P^-1,S) = We have to check termination of S: Matrix Interpretation Processor: dim=1 interpretation: [+](x0, x1) = x0 + x1, [p](x0) = x0 + 6, [0] = 3, [s](x0) = x0 + 1 orientation: +(x,0()) = x + 3 >= x = x +(x,s(y)) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(x,p(y)) = x + y + 6 >= x + y + 6 = p(+(x,y)) +(0(),y) = y + 3 >= y = y +(s(x),y) = x + y + 1 >= x + y + 1 = s(+(x,y)) +(p(x),y) = x + y + 6 >= x + y + 6 = p(+(x,y)) s(p(x)) = x + 7 >= x = x p(s(x)) = x + 7 >= x = x problem: +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(s(x),y) -> s(+(x,y)) +(p(x),y) -> p(+(x,y)) Matrix Interpretation Processor: dim=1 interpretation: [+](x0, x1) = 4x0 + x1 + 7, [p](x0) = x0 + 1, [s](x0) = x0 orientation: +(x,s(y)) = 4x + y + 7 >= 4x + y + 7 = s(+(x,y)) +(x,p(y)) = 4x + y + 8 >= 4x + y + 8 = p(+(x,y)) +(s(x),y) = 4x + y + 7 >= 4x + y + 7 = s(+(x,y)) +(p(x),y) = 4x + y + 11 >= 4x + y + 8 = p(+(x,y)) problem: +(x,s(y)) -> s(+(x,y)) +(x,p(y)) -> p(+(x,y)) +(s(x),y) -> s(+(x,y)) Matrix Interpretation Processor: dim=1 interpretation: [+](x0, x1) = 2x0 + 6x1, [p](x0) = x0, [s](x0) = x0 + 2 orientation: +(x,s(y)) = 2x + 6y + 12 >= 2x + 6y + 2 = s(+(x,y)) +(x,p(y)) = 2x + 6y >= 2x + 6y = p(+(x,y)) +(s(x),y) = 2x + 6y + 4 >= 2x + 6y + 2 = s(+(x,y)) problem: +(x,p(y)) -> p(+(x,y)) Matrix Interpretation Processor: dim=1 interpretation: [+](x0, x1) = x0 + 4x1, [p](x0) = x0 + 5 orientation: +(x,p(y)) = x + 4y + 20 >= x + 4y + 5 = p(+(x,y)) problem: Qed