YES(?,O(n^1))
13.53/3.68	YES(?,O(n^1))
13.53/3.69	
13.53/3.69	Problem:
13.53/3.69	 b(b(x1)) -> a(a(a(x1)))
13.53/3.69	 b(a(b(x1))) -> a(x1)
13.53/3.69	 b(a(a(x1))) -> b(a(b(x1)))
13.53/3.69	
13.53/3.69	Proof:
13.53/3.69	 Complexity Transformation Processor:
13.53/3.69	  strict:
13.53/3.69	   b(b(x1)) -> a(a(a(x1)))
13.53/3.69	   b(a(b(x1))) -> a(x1)
13.53/3.69	   b(a(a(x1))) -> b(a(b(x1)))
13.53/3.69	  weak:
13.53/3.69	   
13.53/3.69	  Matrix Interpretation Processor: dim=1
13.53/3.69	   
13.53/3.69	   max_matrix:
13.53/3.69	    1
13.53/3.69	   interpretation:
13.53/3.69	    [a](x0) = x0 + 132,
13.53/3.69	    
13.53/3.69	    [b](x0) = x0 + 129
13.53/3.69	   orientation:
13.53/3.69	    b(b(x1)) = x1 + 258 >= x1 + 396 = a(a(a(x1)))
13.53/3.69	    
13.53/3.69	    b(a(b(x1))) = x1 + 390 >= x1 + 132 = a(x1)
13.53/3.69	    
13.53/3.69	    b(a(a(x1))) = x1 + 393 >= x1 + 390 = b(a(b(x1)))
13.53/3.69	   problem:
13.53/3.69	    strict:
13.53/3.69	     b(b(x1)) -> a(a(a(x1)))
13.53/3.69	    weak:
13.53/3.69	     b(a(b(x1))) -> a(x1)
13.53/3.69	     b(a(a(x1))) -> b(a(b(x1)))
13.53/3.69	   Arctic Interpretation Processor:
13.53/3.69	    dimension: 3
13.53/3.69	    interpretation:
13.53/3.69	               [0  -& -&]  
13.53/3.69	     [a](x0) = [-& -& 0 ]x0
13.53/3.69	               [-& 0  -&]  ,
13.53/3.69	     
13.53/3.69	               [0  0  -&]  
13.53/3.69	     [b](x0) = [1  1  0 ]x0
13.53/3.69	               [-& 0  -&]  
13.53/3.69	    orientation:
13.53/3.69	                [1 1 0]      [0  -& -&]                
13.53/3.69	     b(b(x1)) = [2 2 1]x1 >= [-& -& 0 ]x1 = a(a(a(x1)))
13.53/3.69	                [1 1 0]      [-& 0  -&]                
13.53/3.69	     
13.53/3.69	                   [0  0  -&]      [0  -& -&]          
13.53/3.69	     b(a(b(x1))) = [1  1  0 ]x1 >= [-& -& 0 ]x1 = a(x1)
13.53/3.69	                   [-& 0  -&]      [-& 0  -&]          
13.53/3.69	     
13.53/3.69	                   [0  0  -&]      [0  0  -&]                
13.53/3.69	     b(a(a(x1))) = [1  1  0 ]x1 >= [1  1  0 ]x1 = b(a(b(x1)))
13.53/3.69	                   [-& 0  -&]      [-& 0  -&]                
13.53/3.69	    problem:
13.53/3.69	     strict:
13.53/3.69	      
13.53/3.69	     weak:
13.53/3.69	      b(b(x1)) -> a(a(a(x1)))
13.53/3.69	      b(a(b(x1))) -> a(x1)
13.53/3.69	      b(a(a(x1))) -> b(a(b(x1)))
13.53/3.69	    Qed
13.53/3.69	EOF