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