YES(?,O(n^1))
8.84/2.41	YES(?,O(n^1))
8.84/2.41	
8.84/2.41	Problem:
8.84/2.41	 a(b(a(x1))) -> b(x1)
8.84/2.41	 b(a(b(x1))) -> b(b(b(x1)))
8.84/2.41	 b(b(x1)) -> a(a(a(x1)))
8.84/2.41	
8.84/2.41	Proof:
8.84/2.41	 Complexity Transformation Processor:
8.84/2.41	  strict:
8.84/2.41	   a(b(a(x1))) -> b(x1)
8.84/2.41	   b(a(b(x1))) -> b(b(b(x1)))
8.84/2.41	   b(b(x1)) -> a(a(a(x1)))
8.84/2.41	  weak:
8.84/2.41	   
8.84/2.41	  Matrix Interpretation Processor: dim=1
8.84/2.41	   
8.84/2.41	   max_matrix:
8.84/2.41	    1
8.84/2.41	   interpretation:
8.84/2.41	    [b](x0) = x0 + 155,
8.84/2.41	    
8.84/2.41	    [a](x0) = x0 + 37
8.84/2.41	   orientation:
8.84/2.41	    a(b(a(x1))) = x1 + 229 >= x1 + 155 = b(x1)
8.84/2.41	    
8.84/2.41	    b(a(b(x1))) = x1 + 347 >= x1 + 465 = b(b(b(x1)))
8.84/2.41	    
8.84/2.41	    b(b(x1)) = x1 + 310 >= x1 + 111 = a(a(a(x1)))
8.84/2.41	   problem:
8.84/2.41	    strict:
8.84/2.41	     b(a(b(x1))) -> b(b(b(x1)))
8.84/2.41	    weak:
8.84/2.41	     a(b(a(x1))) -> b(x1)
8.84/2.41	     b(b(x1)) -> a(a(a(x1)))
8.84/2.41	   Arctic Interpretation Processor:
8.84/2.41	    dimension: 2
8.84/2.41	    interpretation:
8.84/2.41	               [1 0]  
8.84/2.41	     [b](x0) = [2 1]x0,
8.84/2.41	     
8.84/2.41	               [0  1 ]  
8.84/2.41	     [a](x0) = [-& 0 ]x0
8.84/2.41	    orientation:
8.84/2.41	                   [4 3]      [3 2]                
8.84/2.41	     b(a(b(x1))) = [5 4]x1 >= [4 3]x1 = b(b(b(x1)))
8.84/2.41	     
8.84/2.41	                   [3 4]      [1 0]          
8.84/2.41	     a(b(a(x1))) = [2 3]x1 >= [2 1]x1 = b(x1)
8.84/2.41	     
8.84/2.41	                [2 1]      [0  1 ]                
8.84/2.41	     b(b(x1)) = [3 2]x1 >= [-& 0 ]x1 = a(a(a(x1)))
8.84/2.41	    problem:
8.84/2.41	     strict:
8.84/2.41	      
8.84/2.41	     weak:
8.84/2.41	      b(a(b(x1))) -> b(b(b(x1)))
8.84/2.41	      a(b(a(x1))) -> b(x1)
8.84/2.41	      b(b(x1)) -> a(a(a(x1)))
8.84/2.41	    Qed
8.84/2.41	EOF