2.07/1.33	YES
2.07/1.33	
2.07/1.33	Problem:
2.07/1.33	 f(f(x)) -> f(g(f(x),f(x)))
2.07/1.33	
2.07/1.33	Proof:
2.07/1.33	 AT confluence processor
2.07/1.33	  Complete TRS T' of input TRS:
2.07/1.33	  f(f(x)) -> f(g(f(x),f(x)))
2.07/1.33	  
2.07/1.33	   T' = (P union S) with
2.07/1.33	  
2.07/1.33	   TRS P:
2.07/1.33	  
2.07/1.33	   TRS S:f(f(x)) -> f(g(f(x),f(x)))
2.07/1.33	  
2.07/1.33	  S is left-linear and P is reversible.
2.07/1.33	  
2.07/1.33	   CP(S,S) = 
2.07/1.33	  f(f(g(f(x6),f(x6)))) = f(g(f(f(x6)),f(f(x6))))
2.07/1.33	  
2.07/1.33	   CP(S,P union P^-1) = 
2.07/1.33	  
2.07/1.33	  
2.07/1.33	   PCP_in(P union P^-1,S) = 
2.07/1.33	  
2.07/1.33	  
2.07/1.33	  We have to check termination of S:
2.07/1.33	  
2.07/1.33	  Matrix Interpretation Processor: dim=2
2.07/1.33	   
2.07/1.33	   interpretation:
2.07/1.33	                  [2 0]     [1 0]  
2.07/1.33	    [g](x0, x1) = [0 0]x0 + [0 0]x1,
2.07/1.33	    
2.07/1.33	              [1 2]     [0]
2.07/1.33	    [f](x0) = [1 2]x0 + [1]
2.07/1.33	   orientation:
2.07/1.33	              [3 6]    [2]    [3 6]    [0]                  
2.07/1.33	    f(f(x)) = [3 6]x + [3] >= [3 6]x + [1] = f(g(f(x),f(x)))
2.07/1.33	   problem:
2.07/1.33	    
2.07/1.33	   Qed
2.07/1.34	EOF