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