YES(?,O(n^1))
6.64/1.90	YES(?,O(n^1))
6.64/1.90	
6.64/1.90	Problem:
6.64/1.90	 f(n__f(n__a())) -> f(n__g(f(n__a())))
6.64/1.90	 f(X) -> n__f(X)
6.64/1.90	 a() -> n__a()
6.64/1.90	 g(X) -> n__g(X)
6.64/1.90	 activate(n__f(X)) -> f(X)
6.64/1.90	 activate(n__a()) -> a()
6.64/1.90	 activate(n__g(X)) -> g(X)
6.64/1.90	 activate(X) -> X
6.64/1.90	
6.64/1.90	Proof:
6.64/1.90	 Complexity Transformation Processor:
6.64/1.90	  strict:
6.64/1.90	   f(n__f(n__a())) -> f(n__g(f(n__a())))
6.64/1.90	   f(X) -> n__f(X)
6.64/1.90	   a() -> n__a()
6.64/1.90	   g(X) -> n__g(X)
6.64/1.90	   activate(n__f(X)) -> f(X)
6.64/1.90	   activate(n__a()) -> a()
6.64/1.90	   activate(n__g(X)) -> g(X)
6.64/1.90	   activate(X) -> X
6.64/1.90	  weak:
6.64/1.90	   
6.64/1.90	  Matrix Interpretation Processor: dim=1
6.64/1.90	   
6.64/1.90	   max_matrix:
6.64/1.90	    1
6.64/1.90	   interpretation:
6.64/1.90	    [activate](x0) = x0 + 63,
6.64/1.90	    
6.64/1.90	    [g](x0) = x0,
6.64/1.90	    
6.64/1.90	    [a] = 0,
6.64/1.90	    
6.64/1.90	    [n__g](x0) = x0 + 22,
6.64/1.90	    
6.64/1.90	    [f](x0) = x0 + 3,
6.64/1.90	    
6.64/1.90	    [n__f](x0) = x0 + 77,
6.64/1.90	    
6.64/1.90	    [n__a] = 72
6.64/1.90	   orientation:
6.64/1.90	    f(n__f(n__a())) = 152 >= 100 = f(n__g(f(n__a())))
6.64/1.90	    
6.64/1.90	    f(X) = X + 3 >= X + 77 = n__f(X)
6.64/1.90	    
6.64/1.90	    a() = 0 >= 72 = n__a()
6.64/1.90	    
6.64/1.90	    g(X) = X >= X + 22 = n__g(X)
6.64/1.90	    
6.64/1.90	    activate(n__f(X)) = X + 140 >= X + 3 = f(X)
6.64/1.90	    
6.64/1.90	    activate(n__a()) = 135 >= 0 = a()
6.64/1.90	    
6.64/1.90	    activate(n__g(X)) = X + 85 >= X = g(X)
6.64/1.90	    
6.64/1.90	    activate(X) = X + 63 >= X = X
6.64/1.90	   problem:
6.64/1.90	    strict:
6.64/1.90	     f(X) -> n__f(X)
6.64/1.90	     a() -> n__a()
6.64/1.90	     g(X) -> n__g(X)
6.64/1.90	    weak:
6.64/1.90	     f(n__f(n__a())) -> f(n__g(f(n__a())))
6.64/1.90	     activate(n__f(X)) -> f(X)
6.64/1.90	     activate(n__a()) -> a()
6.64/1.90	     activate(n__g(X)) -> g(X)
6.64/1.90	     activate(X) -> X
6.64/1.90	   Matrix Interpretation Processor: dim=1
6.64/1.90	    
6.64/1.90	    max_matrix:
6.64/1.90	     1
6.64/1.90	    interpretation:
6.64/1.90	     [activate](x0) = x0 + 16,
6.64/1.90	     
6.64/1.90	     [g](x0) = x0 + 1,
6.64/1.90	     
6.64/1.90	     [a] = 0,
6.64/1.90	     
6.64/1.90	     [n__g](x0) = x0,
6.64/1.90	     
6.64/1.90	     [f](x0) = x0,
6.64/1.90	     
6.64/1.90	     [n__f](x0) = x0 + 68,
6.64/1.90	     
6.64/1.90	     [n__a] = 56
6.64/1.90	    orientation:
6.64/1.90	     f(X) = X >= X + 68 = n__f(X)
6.64/1.90	     
6.64/1.90	     a() = 0 >= 56 = n__a()
6.64/1.90	     
6.64/1.90	     g(X) = X + 1 >= X = n__g(X)
6.64/1.90	     
6.64/1.90	     f(n__f(n__a())) = 124 >= 56 = f(n__g(f(n__a())))
6.64/1.90	     
6.64/1.90	     activate(n__f(X)) = X + 84 >= X = f(X)
6.64/1.90	     
6.64/1.90	     activate(n__a()) = 72 >= 0 = a()
6.64/1.90	     
6.64/1.90	     activate(n__g(X)) = X + 16 >= X + 1 = g(X)
6.64/1.90	     
6.64/1.90	     activate(X) = X + 16 >= X = X
6.64/1.90	    problem:
6.64/1.90	     strict:
6.64/1.90	      f(X) -> n__f(X)
6.64/1.90	      a() -> n__a()
6.64/1.90	     weak:
6.64/1.90	      g(X) -> n__g(X)
6.64/1.90	      f(n__f(n__a())) -> f(n__g(f(n__a())))
6.64/1.90	      activate(n__f(X)) -> f(X)
6.64/1.90	      activate(n__a()) -> a()
6.64/1.90	      activate(n__g(X)) -> g(X)
6.64/1.90	      activate(X) -> X
6.64/1.90	    Matrix Interpretation Processor: dim=1
6.64/1.90	     
6.64/1.90	     max_matrix:
6.64/1.90	      1
6.64/1.90	     interpretation:
6.64/1.90	      [activate](x0) = x0 + 80,
6.64/1.90	      
6.64/1.90	      [g](x0) = x0 + 48,
6.64/1.90	      
6.64/1.90	      [a] = 128,
6.64/1.90	      
6.64/1.90	      [n__g](x0) = x0 + 34,
6.64/1.90	      
6.64/1.90	      [f](x0) = x0 + 4,
6.64/1.90	      
6.64/1.90	      [n__f](x0) = x0 + 172,
6.64/1.90	      
6.64/1.90	      [n__a] = 66
6.64/1.90	     orientation:
6.64/1.90	      f(X) = X + 4 >= X + 172 = n__f(X)
6.64/1.90	      
6.64/1.90	      a() = 128 >= 66 = n__a()
6.64/1.90	      
6.64/1.90	      g(X) = X + 48 >= X + 34 = n__g(X)
6.64/1.90	      
6.64/1.90	      f(n__f(n__a())) = 242 >= 108 = f(n__g(f(n__a())))
6.64/1.90	      
6.64/1.90	      activate(n__f(X)) = X + 252 >= X + 4 = f(X)
6.64/1.90	      
6.64/1.90	      activate(n__a()) = 146 >= 128 = a()
6.64/1.90	      
6.64/1.90	      activate(n__g(X)) = X + 114 >= X + 48 = g(X)
6.64/1.90	      
6.64/1.90	      activate(X) = X + 80 >= X = X
6.64/1.90	     problem:
6.64/1.90	      strict:
6.64/1.90	       f(X) -> n__f(X)
6.64/1.90	      weak:
6.64/1.90	       a() -> n__a()
6.64/1.90	       g(X) -> n__g(X)
6.64/1.90	       f(n__f(n__a())) -> f(n__g(f(n__a())))
6.64/1.90	       activate(n__f(X)) -> f(X)
6.64/1.90	       activate(n__a()) -> a()
6.64/1.90	       activate(n__g(X)) -> g(X)
6.64/1.90	       activate(X) -> X
6.64/1.90	     Arctic Interpretation Processor:
6.64/1.90	      dimension: 2
6.64/1.90	      interpretation:
6.64/1.90	                        [1 7]  
6.64/1.90	       [activate](x0) = [0 4]x0,
6.64/1.90	       
6.64/1.90	                 [0  5 ]  
6.64/1.90	       [g](x0) = [-& 0 ]x0,
6.64/1.90	       
6.64/1.90	             [7]
6.64/1.90	       [a] = [2],
6.64/1.90	       
6.64/1.90	                    [0  5 ]  
6.64/1.90	       [n__g](x0) = [-& -&]x0,
6.64/1.90	       
6.64/1.90	                 [1  7 ]  
6.64/1.90	       [f](x0) = [-& 2 ]x0,
6.64/1.90	       
6.64/1.90	                    [0  0 ]  
6.64/1.90	       [n__f](x0) = [-& 1 ]x0,
6.64/1.90	       
6.64/1.90	                [0]
6.64/1.90	       [n__a] = [0]
6.64/1.90	      orientation:
6.64/1.90	              [1  7 ]     [0  0 ]           
6.64/1.90	       f(X) = [-& 2 ]X >= [-& 1 ]X = n__f(X)
6.64/1.90	       
6.64/1.90	             [7]    [0]         
6.64/1.90	       a() = [2] >= [0] = n__a()
6.64/1.90	       
6.64/1.90	              [0  5 ]     [0  5 ]           
6.64/1.90	       g(X) = [-& 0 ]X >= [-& -&]X = n__g(X)
6.64/1.90	       
6.64/1.90	                         [8]    [8 ]                     
6.64/1.90	       f(n__f(n__a())) = [3] >= [-&] = f(n__g(f(n__a())))
6.64/1.90	       
6.64/1.90	                           [1 8]     [1  7 ]        
6.64/1.90	       activate(n__f(X)) = [0 5]X >= [-& 2 ]X = f(X)
6.64/1.90	       
6.64/1.90	                          [7]    [7]      
6.64/1.90	       activate(n__a()) = [4] >= [2] = a()
6.64/1.90	       
6.64/1.90	                           [1 6]     [0  5 ]        
6.64/1.90	       activate(n__g(X)) = [0 5]X >= [-& 0 ]X = g(X)
6.64/1.90	       
6.64/1.90	                     [1 7]          
6.64/1.90	       activate(X) = [0 4]X >= X = X
6.64/1.90	      problem:
6.64/1.90	       strict:
6.64/1.90	        
6.64/1.90	       weak:
6.64/1.90	        f(X) -> n__f(X)
6.64/1.90	        a() -> n__a()
6.64/1.90	        g(X) -> n__g(X)
6.64/1.90	        f(n__f(n__a())) -> f(n__g(f(n__a())))
6.64/1.90	        activate(n__f(X)) -> f(X)
6.64/1.90	        activate(n__a()) -> a()
6.64/1.90	        activate(n__g(X)) -> g(X)
6.64/1.90	        activate(X) -> X
6.64/1.90	      Qed
6.64/1.91	EOF