0.00/0.13	YES
0.00/0.13	
0.00/0.13	# Compositional parallel rule labeling (Shintani and Hirokawa 2022).
0.00/0.13	
0.00/0.13	Consider the left-linear TRS R:
0.00/0.13	
0.00/0.13	  f(g(h(x))) -> g(f(h(g(x))))
0.00/0.13	  f(x) -> x
0.00/0.13	  g(x) -> x
0.00/0.13	  h(x) -> x
0.00/0.13	
0.00/0.13	Let C be the following subset of R:
0.00/0.13	
0.00/0.13	  (empty)
0.00/0.13	
0.00/0.13	All parallel critical peaks (except C's) are decreasing wrt rule labeling:
0.00/0.13	
0.00/0.13	  phi(f(g(h(x))) -> g(f(h(g(x))))) = 2
0.00/0.13	  phi(f(x) -> x) = 1
0.00/0.13	  phi(g(x) -> x) = 1
0.00/0.13	  phi(h(x) -> x) = 1
0.00/0.13	
0.00/0.13	  psi(f(g(h(x))) -> g(f(h(g(x))))) = 2
0.00/0.13	  psi(f(x) -> x) = 1
0.00/0.13	  psi(g(x) -> x) = 1
0.00/0.13	  psi(h(x) -> x) = 1
0.00/0.13	
0.00/0.13	
0.00/0.13	Therefore, the confluence of R follows from that of C.
0.00/0.13	
0.00/0.13	# Compositional parallel critical pair system (Shintani and Hirokawa 2022).
0.00/0.13	
0.00/0.13	Consider the left-linear TRS R:
0.00/0.13	
0.00/0.13	  (empty)
0.00/0.13	
0.00/0.13	Let C be the following subset of R:
0.00/0.13	
0.00/0.13	  (empty)
0.00/0.13	
0.00/0.13	The parallel critical pair system PCPS(R,C) is:
0.00/0.13	
0.00/0.13	  (empty)
0.00/0.13	
0.00/0.13	All pairs in PCP(R) are joinable and PCPS(R,C)/R is terminating.
0.00/0.13	Therefore, the confluence of R follows from that of C.
0.00/0.13	
0.00/0.13	# emptiness
0.00/0.13	
0.00/0.13	The empty TRS is confluent.
0.00/0.13	
0.00/0.13	EOF