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(),x503)) = s(x503), s(+(s(x),x505)) = s(+(x,s(x505))), s(+(p(x),x507)) = p(+(x,s(x507))), p(+(0(),x509)) = p(x509), p(+(s(x),x511)) = s(+(x,p(x511))), p(+(p(x),x513)) = p(+(x,p(x513))), s(y) = s(+(0(),y)), p(y) = p(+(0(),y)), s(+(x517,0())) = s(x517), s(+(x519,s(y))) = s(+(s(x519),y)), s(+(x521,p(y))) = p(+(s(x521),y)), p(+(x523,0())) = p(x523), p(+(x525,s(y))) = s(+(p(x525),y)), p(+(x527,p(y))) = p(+(p(x527),y)), +(x,x529) = s(+(x,p(x529))), +(x530,y) = s(+(p(x530),y)), p(x531) = p(x531), +(x,x532) = p(+(x,s(x532))), +(x533,y) = p(+(s(x533),y)), s(x534) = s(x534) CP(S,P union P^-1) = x = +(0(),x), y = +(0(),y), s(+(x,x562)) = +(s(x562),x), s(+(y,x564)) = +(s(x564),y), p(+(x,x566)) = +(p(x566),x), p(+(y,x568)) = +(p(x568),y), y = +(y,0()), x = +(x,0()), s(+(x571,y)) = +(y,s(x571)), s(+(x573,x)) = +(x,s(x573)), p(+(x575,y)) = +(y,p(x575)), p(+(x577,x)) = +(x,p(x577)) 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