YES(?,O(n^1))
11.52/3.19	YES(?,O(n^1))
11.52/3.19	
11.52/3.19	Problem:
11.52/3.19	 a(a(x1)) -> a(b(a(x1)))
11.52/3.19	 b(a(b(x1))) -> a(c(a(x1)))
11.52/3.19	
11.52/3.19	Proof:
11.52/3.19	 Complexity Transformation Processor:
11.52/3.19	  strict:
11.52/3.19	   a(a(x1)) -> a(b(a(x1)))
11.52/3.19	   b(a(b(x1))) -> a(c(a(x1)))
11.52/3.19	  weak:
11.52/3.19	   
11.52/3.19	  Matrix Interpretation Processor: dim=1
11.52/3.19	   
11.52/3.19	   max_matrix:
11.52/3.19	    1
11.52/3.19	   interpretation:
11.52/3.19	    [c](x0) = x0 + 9,
11.52/3.19	    
11.52/3.19	    [b](x0) = x0 + 27,
11.52/3.19	    
11.52/3.19	    [a](x0) = x0 + 41
11.52/3.19	   orientation:
11.52/3.19	    a(a(x1)) = x1 + 82 >= x1 + 109 = a(b(a(x1)))
11.52/3.19	    
11.52/3.19	    b(a(b(x1))) = x1 + 95 >= x1 + 91 = a(c(a(x1)))
11.52/3.19	   problem:
11.52/3.19	    strict:
11.52/3.19	     a(a(x1)) -> a(b(a(x1)))
11.52/3.19	    weak:
11.52/3.19	     b(a(b(x1))) -> a(c(a(x1)))
11.52/3.19	   Arctic Interpretation Processor:
11.52/3.19	    dimension: 3
11.52/3.19	    interpretation:
11.52/3.19	               [0  -& -&]  
11.52/3.19	     [c](x0) = [-& -& -&]x0
11.52/3.19	               [-& -& -&]  ,
11.52/3.19	     
11.52/3.19	               [0  0  1 ]  
11.52/3.19	     [b](x0) = [-& -& 1 ]x0
11.52/3.19	               [0  0  0 ]  ,
11.52/3.19	     
11.52/3.19	               [0  1  0 ]  
11.52/3.19	     [a](x0) = [0  3  2 ]x0
11.52/3.19	               [-& 1  0 ]  
11.52/3.19	    orientation:
11.52/3.19	                [1 4 3]      [0 3 2]                
11.52/3.19	     a(a(x1)) = [3 6 5]x1 >= [2 5 4]x1 = a(b(a(x1)))
11.52/3.19	                [1 4 3]      [0 3 2]                
11.52/3.19	     
11.52/3.19	                   [2 2 4]      [0  1  0 ]                
11.52/3.19	     b(a(b(x1))) = [1 1 3]x1 >= [0  1  0 ]x1 = a(c(a(x1)))
11.52/3.19	                   [2 2 4]      [-& -& -&]                
11.52/3.19	    problem:
11.52/3.19	     strict:
11.52/3.19	      
11.52/3.19	     weak:
11.52/3.19	      a(a(x1)) -> a(b(a(x1)))
11.52/3.19	      b(a(b(x1))) -> a(c(a(x1)))
11.52/3.19	    Qed
11.52/3.20	EOF