5.97/2.22	YES
5.97/2.22	
5.97/2.22	Problem:
5.97/2.23	f(x, x) -> a()
5.97/2.23	g(x) -> a() <= g(x) = b()
5.97/2.23	a() -> b()
5.97/2.23	b() -> a()
5.97/2.23	
5.97/2.23	Proof:
5.97/2.23	This system is confluent.
5.97/2.23	By \cite{GNG13}, Theorem 9.
5.97/2.23	This system is of type 3 or smaller.
5.97/2.23	This system is deterministic.
5.97/2.23	This system is weakly left-linear.
5.97/2.23	System R transformed to optimized U(R).
5.97/2.23	This system is confluent.
5.97/2.23	Call external tool:
5.97/2.23	./csi.sh
5.97/2.23	Input:
5.97/2.23	  f(x, x) -> a()
5.97/2.23	  ?1(b(), x) -> a()
5.97/2.23	  g(x) -> ?1(g(x), x)
5.97/2.23	  a() -> b()
5.97/2.23	  b() -> a()
5.97/2.23	
5.97/2.23	 sorted: (order)
5.97/2.23	 0:f(x,x) -> a()
5.97/2.23	   a() -> b()
5.97/2.23	   b() -> a()
5.97/2.23	 1:?1(b(),x) -> a()
5.97/2.23	   g(x) -> ?1(g(x),x)
5.97/2.23	   a() -> b()
5.97/2.23	   b() -> a()
5.97/2.23	 -----
5.97/2.23	 sorts
5.97/2.23	   [0>2, 0>4, 1>2, 1>3]
5.97/2.23	 sort attachment (strict)
5.97/2.23	   f : 4 x 4 -> 0
5.97/2.23	   a : 2
5.97/2.23	   ?1 : 1 x 3 -> 1
5.97/2.23	   b : 2
5.97/2.23	   g : 3 -> 1
5.97/2.23	 -----
5.97/2.23	 0:f(x,x) -> a()
5.97/2.23	   a() -> b()
5.97/2.23	   b() -> a()
5.97/2.23	   Church Rosser Transformation Processor (to relative problem):
5.97/2.23	    strict:
5.97/2.23	     f(x,x) -> a()
5.97/2.23	     a() -> b()
5.97/2.23	     b() -> a()
5.97/2.23	    weak:
5.97/2.23	     
5.97/2.23	    original problem:
5.97/2.23	     f(x,x) -> a()
5.97/2.23	     a() -> b()
5.97/2.23	     b() -> a()
5.97/2.23	    critical peaks: 
5.97/2.23	     Polynomial Interpretation Processor:
5.97/2.23	      dimension: 1
5.97/2.23	      interpretation:
5.97/2.23	       [b] = 0,
5.97/2.23	       
5.97/2.23	       [a] = 0,
5.97/2.23	       
5.97/2.23	       [f](x0, x1) = x0 + x1 + 2
5.97/2.23	      orientation:
5.97/2.23	       f(x,x) = 2x + 2 >= 0 = a()
5.97/2.23	       
5.97/2.23	       a() = 0 >= 0 = b()
5.97/2.23	       
5.97/2.23	       b() = 0 >= 0 = a()
5.97/2.23	      problem:
5.97/2.23	       strict:
5.97/2.23	        a() -> b()
5.97/2.23	        b() -> a()
5.97/2.23	       weak:
5.97/2.23	        
5.97/2.23	       original problem:
5.97/2.23	        f(x,x) -> a()
5.97/2.23	        a() -> b()
6.59/2.23	        b() -> a()
6.59/2.23	      KH confluence processor
6.59/2.23	       Split input TRS into two TRSs S and T:
6.59/2.23	       
6.59/2.23	       TRS S:
6.59/2.23	        a() -> b()
6.59/2.23	        b() -> a()
6.59/2.23	       
6.59/2.23	       TRS T:
6.59/2.24	        f(x,x) -> a()
6.59/2.24	       
6.59/2.24	       As established above, T/S is terminating.
6.59/2.24	       T is strongly non-overlapping on S and S is strongly non-overlapping on T
6.59/2.24	       
6.59/2.24	       Please install theorem prover 'Prover9' and 'Mace4' for handling more TRSs.
6.59/2.24	       
6.59/2.24	        All S-critical pairs are joinable.
6.59/2.24	       
6.59/2.24	       We have to check confluence of S.
6.59/2.24	       
6.59/2.24	       Church Rosser Transformation Processor:
6.59/2.24	        strict:
6.59/2.24	         a() -> b()
6.59/2.24	         b() -> a()
6.59/2.24	        weak:
6.59/2.24	         
6.59/2.24	        critical peaks: 0
6.59/2.24	        Closedness Processor (*strongly -- <=7 steps*):
6.59/2.24	         strict:
6.59/2.24	          
6.59/2.24	         weak:
6.59/2.24	          
6.59/2.24	         Qed
6.59/2.24	 
6.59/2.24	 
6.59/2.24	 1:?1(b(),x) -> a()
6.59/2.24	   g(x) -> ?1(g(x),x)
6.59/2.24	   a() -> b()
6.59/2.24	   b() -> a()
6.59/2.24	   Church Rosser Transformation Processor:
6.59/2.24	    strict:
6.59/2.24	     
6.59/2.24	    weak:
6.59/2.24	     
6.59/2.24	    critical peaks: 1
6.59/2.24	     ?1(a(),x) <-3|0[]- ?1(b(),x) -0|[]-> a()
6.59/2.24	    Shift Processor lab=left (dd) (force):
6.59/2.24	     strict:
6.59/2.24	      ?1(b(),x) -> ?1(a(),x)
6.59/2.24	      ?1(b(),x) -> a()
6.59/2.24	      ?1(a(),x) -> ?1(b(),x)
6.59/2.24	      ?1(b(),x) -> a()
6.59/2.24	     weak:
6.59/2.24	      ?1(b(),x) -> a()
6.59/2.24	      g(x) -> ?1(g(x),x)
6.59/2.24	      a() -> b()
6.59/2.24	      b() -> a()
6.59/2.24	     Shift Processor (ldh) lab=left (force):
6.59/2.24	      strict:
6.59/2.24	       
6.59/2.24	      weak:
6.59/2.24	       
6.59/2.24	      Rule Labeling Processor:
6.59/2.24	       strict:
6.59/2.24	        
6.59/2.24	       weak:
6.59/2.24	        
6.59/2.24	       rule labeling (right):
6.59/2.24	        ?1(b(),x) -> a(): 0
6.59/2.24	        g(x) -> ?1(g(x),x): 0
6.59/2.24	        a() -> b(): 0
6.59/2.24	        b() -> a(): 1
6.59/2.24	       Rule Labeling Processor:
6.59/2.24	        strict:
6.59/2.24	         
6.59/2.24	        weak:
6.59/2.24	         
6.59/2.24	        rule labeling (left):
6.59/2.24	         ?1(b(),x) -> a(): 0
6.59/2.24	         g(x) -> ?1(g(x),x): 0
6.59/2.24	         a() -> b(): 0
6.59/2.24	         b() -> a(): 0
6.59/2.24	        Decreasing Processor:
6.59/2.24	         The following diagrams are decreasing:
6.59/2.24	         peak:
6.59/2.24	          ?1(a(),x) <-3|0[==0,==1,=?1]- ?1(b(),x) -0|[==0,==1,>=0]-> a()
6.59/2.24	         joins (1):
6.59/2.24	          ?1(a(),x) -2|0[==0,==1,>=0]-> ?1(b(),x) -0|[==0,==1,>=0]-> a()
6.59/2.24	          
6.59/2.24	         Qed
6.59/2.24	  
6.59/2.24	
6.59/2.25	EOF