0.53/0.69	YES
0.53/0.69	
0.53/0.69	Problem:
0.53/0.69	 H(H(x)) -> K(x)
0.53/0.69	 H(K(x)) -> K(H(x))
0.53/0.69	
0.53/0.69	Proof:
0.53/0.69	 AT confluence processor
0.53/0.69	  Complete TRS T' of input TRS:
0.53/0.69	  H(H(x)) -> K(x)
0.53/0.69	  H(K(x)) -> K(H(x))
0.53/0.69	  
0.53/0.69	   T' = (P union S) with
0.53/0.69	  
0.53/0.69	   TRS P:
0.53/0.69	  
0.53/0.69	   TRS S:H(H(x)) -> K(x)
0.53/0.69	         H(K(x)) -> K(H(x))
0.53/0.69	  
0.53/0.69	  S is left-linear and P is reversible.
0.53/0.69	  
0.53/0.69	   CP(S,S) = 
0.53/0.69	  H(K(x19)) = K(H(x19)), H(K(H(x20))) = K(K(x20))
0.53/0.69	  
0.53/0.69	   CP(S,P union P^-1) = 
0.53/0.69	  
0.53/0.69	  
0.53/0.69	   PCP_in(P union P^-1,S) = 
0.53/0.69	  
0.53/0.69	  
0.53/0.69	  We have to check termination of S:
0.53/0.69	  
0.53/0.69	  Matrix Interpretation Processor: dim=1
0.53/0.69	   
0.53/0.69	   interpretation:
0.53/0.69	    [K](x0) = 4x0 + 6,
0.53/0.69	    
0.53/0.69	    [H](x0) = 5x0 + 1
0.53/0.69	   orientation:
0.53/0.69	    H(H(x)) = 25x + 6 >= 4x + 6 = K(x)
0.53/0.69	    
0.53/0.69	    H(K(x)) = 20x + 31 >= 20x + 10 = K(H(x))
0.53/0.69	   problem:
0.53/0.69	    H(H(x)) -> K(x)
0.53/0.69	   Matrix Interpretation Processor: dim=1
0.53/0.69	    
0.53/0.69	    interpretation:
0.53/0.69	     [K](x0) = 4x0,
0.53/0.69	     
0.53/0.69	     [H](x0) = 2x0 + 1
0.53/0.69	    orientation:
0.53/0.69	     H(H(x)) = 4x + 3 >= 4x = K(x)
0.53/0.69	    problem:
0.53/0.69	     
0.53/0.69	    Qed
0.53/0.69	EOF