8.19/3.27	YES
8.19/3.27	
8.19/3.27	Problem:
8.19/3.27	 a(a(x)) -> a(b(a(x)))
8.19/3.27	 b(a(b(x))) -> a(c(a(x)))
8.19/3.27	
8.19/3.27	Proof:
8.19/3.27	 AT confluence processor
8.19/3.27	  Complete TRS T' of input TRS:
8.19/3.27	  a(a(x)) -> a(b(a(x)))
8.19/3.27	  b(a(b(x))) -> a(c(a(x)))
8.19/3.27	  
8.19/3.27	   T' = (P union S) with
8.19/3.27	  
8.19/3.27	   TRS P:
8.19/3.27	  
8.19/3.27	   TRS S:a(a(x)) -> a(b(a(x)))
8.19/3.27	         b(a(b(x))) -> a(c(a(x)))
8.19/3.27	  
8.19/3.27	  S is left-linear and P is reversible.
8.19/3.27	  
8.19/3.27	   CP(S,S) = 
8.19/3.27	  a(a(b(a(x23)))) = a(b(a(a(x23)))), b(a(a(c(a(x24))))) = a(c(a(a(b(x24)))))
8.19/3.27	  
8.19/3.27	   CP(S,P union P^-1) = 
8.19/3.27	  
8.19/3.27	  
8.19/3.27	   PCP_in(P union P^-1,S) = 
8.19/3.27	  
8.19/3.27	  
8.19/3.27	  We have to check termination of S:
8.19/3.27	  
8.19/3.27	  Matrix Interpretation Processor: dim=3
8.19/3.27	   
8.19/3.27	   interpretation:
8.19/3.27	              [1 0 1]     [0]
8.19/3.27	    [b](x0) = [0 0 0]x0 + [1]
8.19/3.27	              [0 0 0]     [0],
8.19/3.27	    
8.19/3.27	              [1 0 1]     [0]
8.19/3.27	    [a](x0) = [0 0 0]x0 + [1]
8.19/3.27	              [0 1 0]     [0],
8.19/3.27	    
8.19/3.27	              [1 0 0]  
8.19/3.27	    [c](x0) = [0 0 0]x0
8.19/3.27	              [0 0 0]  
8.19/3.27	   orientation:
8.19/3.27	              [1 1 1]    [0]    [1 1 1]    [0]             
8.19/3.27	    a(a(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = a(b(a(x)))
8.19/3.27	              [0 0 0]    [1]    [0 0 0]    [1]             
8.19/3.27	    
8.19/3.27	                 [1 0 1]    [1]    [1 0 1]    [0]             
8.19/3.27	    b(a(b(x))) = [0 0 0]x + [1] >= [0 0 0]x + [1] = a(c(a(x)))
8.19/3.27	                 [0 0 0]    [0]    [0 0 0]    [0]             
8.19/3.27	   problem:
8.19/3.27	    a(a(x)) -> a(b(a(x)))
8.19/3.27	   Matrix Interpretation Processor: dim=2
8.19/3.27	    
8.19/3.27	    interpretation:
8.19/3.27	               [2 0]     [2]
8.19/3.27	     [b](x0) = [0 0]x0 + [0],
8.19/3.27	     
8.19/3.27	               [1 1]     [0]
8.19/3.27	     [a](x0) = [1 1]x0 + [3]
8.19/3.27	    orientation:
8.19/3.27	               [2 2]    [3]    [2 2]    [2]             
8.19/3.27	     a(a(x)) = [2 2]x + [6] >= [2 2]x + [5] = a(b(a(x)))
8.19/3.27	    problem:
8.19/3.27	     
8.19/3.27	    Qed
8.19/3.27	EOF