YES # Compositional parallel rule labeling (Shintani and Hirokawa 2022). Consider the left-linear TRS R: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) +(0(),y) -> y +(s(x),y) -> s(+(x,y)) *(x,0()) -> 0() *(x,s(y)) -> +(*(x,y),x) *(0(),y) -> 0() *(s(x),y) -> +(*(x,y),y) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) Let C be the following subset of R: (empty) All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(+(x,0()) -> x) = 7 phi(+(x,s(y)) -> s(+(x,y))) = 2 phi(+(0(),y) -> y) = 6 phi(+(s(x),y) -> s(+(x,y))) = 1 phi(*(x,0()) -> 0()) = 8 phi(*(x,s(y)) -> +(*(x,y),x)) = 10 phi(*(0(),y) -> 0()) = 8 phi(*(s(x),y) -> +(*(x,y),y)) = 10 phi(+(+(x,y),z) -> +(x,+(y,z))) = 4 phi(+(x,y) -> +(y,x)) = 5 psi(+(x,0()) -> x) = 4 psi(+(x,s(y)) -> s(+(x,y))) = 3 psi(+(0(),y) -> y) = 3 psi(+(s(x),y) -> s(+(x,y))) = 2 psi(*(x,0()) -> 0()) = 5 psi(*(x,s(y)) -> +(*(x,y),x)) = 9 psi(*(0(),y) -> 0()) = 5 psi(*(s(x),y) -> +(*(x,y),y)) = 9 psi(+(+(x,y),z) -> +(x,+(y,z))) = 8 psi(+(x,y) -> +(y,x)) = 8 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.