YES # Compositional parallel rule labeling (Shintani and Hirokawa 2022). Consider the left-linear TRS R: +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) +(s(x),y) -> +(x,s(y)) +(x,s(y)) -> +(s(x),y) *(x,s(y)) -> +(x,*(x,y)) *(s(x),y) -> +(*(x,y),y) *(x,y) -> *(y,x) sq(x) -> *(x,x) sq(s(x)) -> +(*(x,x),s(+(x,x))) Let C be the following subset of R: (empty) All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(+(x,+(y,z)) -> +(+(x,y),z)) = 7 phi(+(+(x,y),z) -> +(x,+(y,z))) = 2 phi(+(x,y) -> +(y,x)) = 2 phi(+(s(x),y) -> +(x,s(y))) = 1 phi(+(x,s(y)) -> +(s(x),y)) = 5 phi(*(x,s(y)) -> +(x,*(x,y))) = 10 phi(*(s(x),y) -> +(*(x,y),y)) = 11 phi(*(x,y) -> *(y,x)) = 13 phi(sq(x) -> *(x,x)) = 15 phi(sq(s(x)) -> +(*(x,x),s(+(x,x)))) = 14 psi(+(x,+(y,z)) -> +(+(x,y),z)) = 8 psi(+(+(x,y),z) -> +(x,+(y,z))) = 6 psi(+(x,y) -> +(y,x)) = 4 psi(+(s(x),y) -> +(x,s(y))) = 9 psi(+(x,s(y)) -> +(s(x),y)) = 3 psi(*(x,s(y)) -> +(x,*(x,y))) = 12 psi(*(s(x),y) -> +(*(x,y),y)) = 14 psi(*(x,y) -> *(y,x)) = 12 psi(sq(x) -> *(x,x)) = 14 psi(sq(s(x)) -> +(*(x,x),s(+(x,x)))) = 15 Therefore, the confluence of R follows from that of C. # Compositional parallel critical pair system (Shintani and Hirokawa 2022). Consider the left-linear TRS R: (empty) Let C be the following subset of R: (empty) The parallel critical pair system PCPS(R,C) is: (empty) All pairs in PCP(R) are joinable and PCPS(R,C)/R is terminating. Therefore, the confluence of R follows from that of C. # emptiness The empty TRS is confluent.