YES(?,O(n^1))
6.00/1.75	YES(?,O(n^1))
6.00/1.75	
6.00/1.75	Problem:
6.00/1.75	 b(b(b(x1))) -> a(x1)
6.00/1.75	 a(a(a(x1))) -> b(b(x1))
6.00/1.75	 a(a(x1)) -> a(b(a(x1)))
6.00/1.75	
6.00/1.75	Proof:
6.00/1.75	 Complexity Transformation Processor:
6.00/1.75	  strict:
6.00/1.75	   b(b(b(x1))) -> a(x1)
6.00/1.75	   a(a(a(x1))) -> b(b(x1))
6.00/1.75	   a(a(x1)) -> a(b(a(x1)))
6.00/1.75	  weak:
6.00/1.75	   
6.00/1.75	  Matrix Interpretation Processor: dim=1
6.00/1.75	   
6.00/1.75	   max_matrix:
6.00/1.75	    1
6.00/1.75	   interpretation:
6.00/1.75	    [a](x0) = x0 + 16,
6.00/1.75	    
6.00/1.75	    [b](x0) = x0 + 40
6.00/1.75	   orientation:
6.00/1.75	    b(b(b(x1))) = x1 + 120 >= x1 + 16 = a(x1)
6.00/1.75	    
6.00/1.75	    a(a(a(x1))) = x1 + 48 >= x1 + 80 = b(b(x1))
6.00/1.75	    
6.00/1.75	    a(a(x1)) = x1 + 32 >= x1 + 72 = a(b(a(x1)))
6.00/1.75	   problem:
6.00/1.75	    strict:
6.00/1.75	     a(a(a(x1))) -> b(b(x1))
6.00/1.75	     a(a(x1)) -> a(b(a(x1)))
6.00/1.75	    weak:
6.00/1.75	     b(b(b(x1))) -> a(x1)
6.00/1.75	   Matrix Interpretation Processor: dim=1
6.00/1.75	    
6.00/1.75	    max_matrix:
6.00/1.75	     1
6.00/1.75	    interpretation:
6.00/1.75	     [a](x0) = x0 + 35,
6.00/1.75	     
6.00/1.75	     [b](x0) = x0 + 35
6.00/1.75	    orientation:
6.00/1.75	     a(a(a(x1))) = x1 + 105 >= x1 + 70 = b(b(x1))
6.00/1.75	     
6.00/1.75	     a(a(x1)) = x1 + 70 >= x1 + 105 = a(b(a(x1)))
6.00/1.75	     
6.00/1.75	     b(b(b(x1))) = x1 + 105 >= x1 + 35 = a(x1)
6.00/1.75	    problem:
6.00/1.75	     strict:
6.00/1.75	      a(a(x1)) -> a(b(a(x1)))
6.00/1.75	     weak:
6.00/1.75	      a(a(a(x1))) -> b(b(x1))
6.00/1.75	      b(b(b(x1))) -> a(x1)
6.00/1.75	    Arctic Interpretation Processor:
6.00/1.75	     dimension: 2
6.00/1.75	     interpretation:
6.00/1.75	                [0 2]  
6.00/1.75	      [a](x0) = [2 4]x0,
6.00/1.75	      
6.00/1.75	                [3  1 ]  
6.00/1.75	      [b](x0) = [0  -&]x0
6.00/1.75	     orientation:
6.00/1.75	                 [4 6]      [3 5]                
6.00/1.75	      a(a(x1)) = [6 8]x1 >= [5 7]x1 = a(b(a(x1)))
6.00/1.75	      
6.00/1.75	                    [8  10]      [6 4]             
6.00/1.75	      a(a(a(x1))) = [10 12]x1 >= [3 1]x1 = b(b(x1))
6.00/1.75	      
6.00/1.75	                    [9 7]      [0 2]          
6.00/1.75	      b(b(b(x1))) = [6 4]x1 >= [2 4]x1 = a(x1)
6.00/1.75	     problem:
6.00/1.75	      strict:
6.00/1.75	       
6.00/1.75	      weak:
6.00/1.75	       a(a(x1)) -> a(b(a(x1)))
6.00/1.75	       a(a(a(x1))) -> b(b(x1))
6.00/1.75	       b(b(b(x1))) -> a(x1)
6.00/1.75	     Qed
6.00/1.76	EOF