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