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