YES # Compositional parallel rule labeling (Shintani and Hirokawa 2022). Consider the left-linear TRS R: P(x) -> Q(Q(p(x))) p(p(x)) -> q(q(x)) p(Q(Q(x))) -> Q(Q(p(x))) Q(p(q(x))) -> q(p(Q(x))) q(q(p(x))) -> p(q(q(x))) q(Q(x)) -> x Q(q(x)) -> x p(P(x)) -> x P(p(x)) -> x Let C be the following subset of R: P(x) -> Q(Q(p(x))) p(p(x)) -> q(q(x)) p(Q(Q(x))) -> Q(Q(p(x))) Q(p(q(x))) -> q(p(Q(x))) q(q(p(x))) -> p(q(q(x))) q(Q(x)) -> x Q(q(x)) -> x p(P(x)) -> x P(p(x)) -> x All parallel critical peaks (except C's) are decreasing wrt rule labeling: phi(P(x) -> Q(Q(p(x)))) = 0 phi(p(p(x)) -> q(q(x))) = 0 phi(p(Q(Q(x))) -> Q(Q(p(x)))) = 0 phi(Q(p(q(x))) -> q(p(Q(x)))) = 0 phi(q(q(p(x))) -> p(q(q(x)))) = 0 phi(q(Q(x)) -> x) = 0 phi(Q(q(x)) -> x) = 0 phi(p(P(x)) -> x) = 0 phi(P(p(x)) -> x) = 0 psi(P(x) -> Q(Q(p(x)))) = 0 psi(p(p(x)) -> q(q(x))) = 0 psi(p(Q(Q(x))) -> Q(Q(p(x)))) = 0 psi(Q(p(q(x))) -> q(p(Q(x)))) = 0 psi(q(q(p(x))) -> p(q(q(x)))) = 0 psi(q(Q(x)) -> x) = 0 psi(Q(q(x)) -> x) = 0 psi(p(P(x)) -> x) = 0 psi(P(p(x)) -> x) = 0 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: P(x) -> Q(Q(p(x))) p(p(x)) -> q(q(x)) p(Q(Q(x))) -> Q(Q(p(x))) Q(p(q(x))) -> q(p(Q(x))) q(q(p(x))) -> p(q(q(x))) q(Q(x)) -> x Q(q(x)) -> x p(P(x)) -> x P(p(x)) -> x Let C be the following subset of R: (empty) The parallel critical pair system PCPS(R,C) is: P(p(x0_1)) -> x0_1 P(p(x0_1)) -> Q(Q(p(p(x0_1)))) p(p(p(x1_1))) -> p(q(q(x1_1))) p(p(p(x1_1))) -> q(q(p(x1_1))) p(p(Q(Q(x1_1)))) -> p(Q(Q(p(x1_1)))) p(p(Q(Q(x1_1)))) -> q(q(Q(Q(x1_1)))) p(p(P(x1_1))) -> p(x1_1) p(p(P(x1_1))) -> q(q(P(x1_1))) p(Q(Q(p(q(x2_1))))) -> p(Q(q(p(Q(x2_1))))) p(Q(Q(p(q(x2_1))))) -> Q(Q(p(p(q(x2_1))))) p(Q(Q(q(x2_1)))) -> p(Q(x2_1)) p(Q(Q(q(x2_1)))) -> Q(Q(p(q(x2_1)))) Q(p(q(q(p(x2_1))))) -> Q(p(p(q(q(x2_1))))) Q(p(q(q(p(x2_1))))) -> q(p(Q(q(p(x2_1))))) Q(p(q(Q(x2_1)))) -> Q(p(x2_1)) Q(p(q(Q(x2_1)))) -> q(p(Q(Q(x2_1)))) q(q(p(p(x2_1)))) -> q(q(q(q(x2_1)))) q(q(p(p(x2_1)))) -> p(q(q(p(x2_1)))) q(q(p(Q(Q(x2_1))))) -> q(q(Q(Q(p(x2_1))))) q(q(p(Q(Q(x2_1))))) -> p(q(q(Q(Q(x2_1))))) q(q(p(P(x2_1)))) -> q(q(x2_1)) q(q(p(P(x2_1)))) -> p(q(q(P(x2_1)))) q(Q(p(q(x1_1)))) -> q(q(p(Q(x1_1)))) q(Q(p(q(x1_1)))) -> p(q(x1_1)) Q(q(q(p(x1_1)))) -> Q(p(q(q(x1_1)))) Q(q(q(p(x1_1)))) -> q(p(x1_1)) p(P(y1)) -> p(Q(Q(p(y1)))) p(P(y1)) -> y1 P(p(y1)) -> Q(Q(p(p(y1)))) P(p(y1)) -> y1 P(p(p(x1_1))) -> P(q(q(x1_1))) P(p(p(x1_1))) -> p(x1_1) P(p(Q(Q(x1_1)))) -> P(Q(Q(p(x1_1)))) P(p(Q(Q(x1_1)))) -> Q(Q(x1_1)) 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.