YES # Compositional parallel rule labeling (Shintani and Hirokawa 2022). Consider the left-linear TRS R: H(I(x)) -> K(J(x)) J(x) -> K(J(x)) I(x) -> I(J(x)) J(x) -> J(K(J(x))) Let C be the following subset of R: (empty) All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(H(I(x)) -> K(J(x))) = 2 phi(J(x) -> K(J(x))) = 1 phi(I(x) -> I(J(x))) = 3 phi(J(x) -> J(K(J(x)))) = 1 psi(H(I(x)) -> K(J(x))) = 2 psi(J(x) -> K(J(x))) = 1 psi(I(x) -> I(J(x))) = 3 psi(J(x) -> J(K(J(x)))) = 1 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) The TRS R is locally confluent and PCPS(R,C)/R is terminating. Therefore, the confluence of R follows from that of C. # Emptiness. The empty TRS is confluent.