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