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	  or(true(),true()) -> true()
0.00/0.13	  or(x,y) -> or(y,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(or(true(),true()) -> true()) = 1
0.00/0.13	  phi(or(x,y) -> or(y,x)) = 1
0.00/0.13	
0.00/0.13	  psi(or(true(),true()) -> true()) = 1
0.00/0.13	  psi(or(x,y) -> or(y,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