YES(?,O(n^1))
6.84/1.90	YES(?,O(n^1))
6.84/1.90	
6.84/1.90	Problem:
6.84/1.90	 b(b(b(x1))) -> a(x1)
6.84/1.90	 a(a(x1)) -> a(b(a(x1)))
6.84/1.90	 a(a(a(x1))) -> b(a(a(x1)))
6.84/1.90	
6.84/1.90	Proof:
6.84/1.90	 Complexity Transformation Processor:
6.84/1.90	  strict:
6.84/1.90	   b(b(b(x1))) -> a(x1)
6.84/1.90	   a(a(x1)) -> a(b(a(x1)))
6.84/1.90	   a(a(a(x1))) -> b(a(a(x1)))
6.84/1.90	  weak:
6.84/1.90	   
6.84/1.90	  Matrix Interpretation Processor: dim=1
6.84/1.90	   
6.84/1.90	   max_matrix:
6.84/1.90	    1
6.84/1.90	   interpretation:
6.84/1.90	    [a](x0) = x0 + 2,
6.84/1.90	    
6.84/1.90	    [b](x0) = x0 + 128
6.84/1.90	   orientation:
6.84/1.90	    b(b(b(x1))) = x1 + 384 >= x1 + 2 = a(x1)
6.84/1.90	    
6.84/1.90	    a(a(x1)) = x1 + 4 >= x1 + 132 = a(b(a(x1)))
6.84/1.90	    
6.84/1.90	    a(a(a(x1))) = x1 + 6 >= x1 + 132 = b(a(a(x1)))
6.84/1.90	   problem:
6.84/1.90	    strict:
6.84/1.90	     a(a(x1)) -> a(b(a(x1)))
6.84/1.90	     a(a(a(x1))) -> b(a(a(x1)))
6.84/1.90	    weak:
6.84/1.90	     b(b(b(x1))) -> a(x1)
6.84/1.90	   Matrix Interpretation Processor: dim=1
6.84/1.90	    
6.84/1.90	    max_matrix:
6.84/1.90	     1
6.84/1.90	    interpretation:
6.84/1.90	     [a](x0) = x0 + 22,
6.84/1.90	     
6.84/1.90	     [b](x0) = x0 + 10
6.84/1.90	    orientation:
6.84/1.90	     a(a(x1)) = x1 + 44 >= x1 + 54 = a(b(a(x1)))
6.84/1.90	     
6.84/1.90	     a(a(a(x1))) = x1 + 66 >= x1 + 54 = b(a(a(x1)))
6.84/1.90	     
6.84/1.90	     b(b(b(x1))) = x1 + 30 >= x1 + 22 = a(x1)
6.84/1.90	    problem:
6.84/1.90	     strict:
6.84/1.90	      a(a(x1)) -> a(b(a(x1)))
6.84/1.90	     weak:
6.84/1.90	      a(a(a(x1))) -> b(a(a(x1)))
6.84/1.90	      b(b(b(x1))) -> a(x1)
6.84/1.90	    Arctic Interpretation Processor:
6.84/1.90	     dimension: 2
6.84/1.90	     interpretation:
6.84/1.90	                [0 2]  
6.84/1.90	      [a](x0) = [1 3]x0,
6.84/1.90	      
6.84/1.90	                [2  1 ]  
6.84/1.90	      [b](x0) = [0  -&]x0
6.84/1.90	     orientation:
6.84/1.90	                 [3 5]      [2 4]                
6.84/1.90	      a(a(x1)) = [4 6]x1 >= [3 5]x1 = a(b(a(x1)))
6.84/1.90	      
6.84/1.90	                    [6 8]      [5 7]                
6.84/1.90	      a(a(a(x1))) = [7 9]x1 >= [3 5]x1 = b(a(a(x1)))
6.84/1.90	      
6.84/1.90	                    [6 5]      [0 2]          
6.84/1.90	      b(b(b(x1))) = [4 3]x1 >= [1 3]x1 = a(x1)
6.84/1.90	     problem:
6.84/1.90	      strict:
6.84/1.90	       
6.84/1.90	      weak:
6.84/1.90	       a(a(x1)) -> a(b(a(x1)))
6.84/1.90	       a(a(a(x1))) -> b(a(a(x1)))
6.84/1.90	       b(b(b(x1))) -> a(x1)
6.84/1.90	     Qed
6.84/1.91	EOF