YES(?,O(n^2))
12.71/6.20	YES(?,O(n^2))
12.71/6.20	
12.71/6.20	Problem:
12.71/6.20	 f(f(a())) -> f(g(n__f(n__a())))
12.71/6.20	 f(X) -> n__f(X)
12.71/6.20	 a() -> n__a()
12.71/6.20	 activate(n__f(X)) -> f(activate(X))
12.71/6.20	 activate(n__a()) -> a()
12.71/6.20	 activate(X) -> X
12.71/6.20	
12.71/6.20	Proof:
12.71/6.20	 Complexity Transformation Processor:
12.71/6.20	  strict:
12.71/6.20	   f(f(a())) -> f(g(n__f(n__a())))
12.71/6.20	   f(X) -> n__f(X)
12.71/6.20	   a() -> n__a()
12.71/6.20	   activate(n__f(X)) -> f(activate(X))
12.71/6.20	   activate(n__a()) -> a()
12.71/6.20	   activate(X) -> X
12.71/6.20	  weak:
12.71/6.20	   
12.71/6.20	  Matrix Interpretation Processor: dim=1
12.71/6.20	   
12.71/6.20	   max_matrix:
12.71/6.20	    1
12.71/6.20	   interpretation:
12.71/6.20	    [activate](x0) = x0 + 57,
12.71/6.20	    
12.71/6.20	    [g](x0) = x0 + 18,
12.71/6.20	    
12.71/6.20	    [n__f](x0) = x0 + 4,
12.71/6.20	    
12.71/6.20	    [n__a] = 12,
12.71/6.20	    
12.71/6.20	    [f](x0) = x0 + 95,
12.71/6.20	    
12.71/6.20	    [a] = 130
12.71/6.20	   orientation:
12.71/6.20	    f(f(a())) = 320 >= 129 = f(g(n__f(n__a())))
12.71/6.20	    
12.71/6.20	    f(X) = X + 95 >= X + 4 = n__f(X)
12.71/6.20	    
12.71/6.20	    a() = 130 >= 12 = n__a()
12.71/6.20	    
12.71/6.20	    activate(n__f(X)) = X + 61 >= X + 152 = f(activate(X))
12.71/6.20	    
12.71/6.20	    activate(n__a()) = 69 >= 130 = a()
12.71/6.20	    
12.71/6.20	    activate(X) = X + 57 >= X = X
12.71/6.20	   problem:
12.71/6.20	    strict:
12.71/6.20	     activate(n__f(X)) -> f(activate(X))
12.71/6.20	     activate(n__a()) -> a()
12.71/6.20	    weak:
12.71/6.20	     f(f(a())) -> f(g(n__f(n__a())))
12.71/6.20	     f(X) -> n__f(X)
12.71/6.20	     a() -> n__a()
12.71/6.20	     activate(X) -> X
12.71/6.20	   Matrix Interpretation Processor: dim=1
12.71/6.20	    
12.71/6.20	    max_matrix:
12.71/6.20	     1
12.71/6.20	    interpretation:
12.71/6.20	     [activate](x0) = x0 + 8,
12.71/6.20	     
12.71/6.20	     [g](x0) = x0,
12.71/6.20	     
12.71/6.20	     [n__f](x0) = x0 + 6,
12.71/6.20	     
12.71/6.20	     [n__a] = 2,
12.71/6.20	     
12.71/6.20	     [f](x0) = x0 + 6,
12.71/6.20	     
12.71/6.20	     [a] = 2
12.71/6.20	    orientation:
12.71/6.20	     activate(n__f(X)) = X + 14 >= X + 14 = f(activate(X))
12.71/6.20	     
12.71/6.20	     activate(n__a()) = 10 >= 2 = a()
12.71/6.20	     
12.71/6.20	     f(f(a())) = 14 >= 14 = f(g(n__f(n__a())))
12.71/6.20	     
12.71/6.20	     f(X) = X + 6 >= X + 6 = n__f(X)
12.71/6.20	     
12.71/6.20	     a() = 2 >= 2 = n__a()
12.71/6.20	     
12.71/6.20	     activate(X) = X + 8 >= X = X
12.71/6.20	    problem:
12.71/6.20	     strict:
12.71/6.20	      activate(n__f(X)) -> f(activate(X))
12.71/6.20	     weak:
12.71/6.20	      activate(n__a()) -> a()
12.71/6.20	      f(f(a())) -> f(g(n__f(n__a())))
12.71/6.20	      f(X) -> n__f(X)
12.71/6.20	      a() -> n__a()
12.71/6.20	      activate(X) -> X
12.71/6.20	    Matrix Interpretation Processor: dim=2
12.71/6.20	     
12.71/6.20	     max_matrix:
12.71/6.20	      [1 1]
12.71/6.20	      [0 1]
12.71/6.20	     interpretation:
12.71/6.20	                       [1 1]  
12.71/6.20	      [activate](x0) = [0 1]x0,
12.71/6.20	      
12.71/6.20	                [1 0]     [0]
12.71/6.20	      [g](x0) = [0 0]x0 + [5],
12.71/6.20	      
12.71/6.20	                   [1 1]     [2]
12.71/6.20	      [n__f](x0) = [0 1]x0 + [5],
12.71/6.20	      
12.71/6.20	               [0]
12.71/6.20	      [n__a] = [0],
12.71/6.20	      
12.71/6.20	                [1 1]     [2]
12.71/6.20	      [f](x0) = [0 1]x0 + [5],
12.71/6.20	      
12.71/6.20	            [0]
12.71/6.20	      [a] = [0]
12.71/6.20	     orientation:
12.71/6.20	                          [1 2]    [7]    [1 2]    [2]                 
12.71/6.20	      activate(n__f(X)) = [0 1]X + [5] >= [0 1]X + [5] = f(activate(X))
12.71/6.20	      
12.71/6.20	                         [0]    [0]      
12.71/6.20	      activate(n__a()) = [0] >= [0] = a()
12.71/6.20	      
12.71/6.20	                  [9 ]    [9 ]                     
12.71/6.20	      f(f(a())) = [10] >= [10] = f(g(n__f(n__a())))
12.71/6.20	      
12.71/6.20	             [1 1]    [2]    [1 1]    [2]          
12.71/6.20	      f(X) = [0 1]X + [5] >= [0 1]X + [5] = n__f(X)
12.71/6.20	      
12.71/6.20	            [0]    [0]         
12.71/6.20	      a() = [0] >= [0] = n__a()
12.71/6.20	      
12.71/6.20	                    [1 1]          
12.71/6.20	      activate(X) = [0 1]X >= X = X
12.71/6.20	     problem:
12.71/6.20	      strict:
12.71/6.20	       
12.71/6.20	      weak:
12.71/6.20	       activate(n__f(X)) -> f(activate(X))
12.71/6.20	       activate(n__a()) -> a()
12.71/6.20	       f(f(a())) -> f(g(n__f(n__a())))
12.71/6.20	       f(X) -> n__f(X)
12.71/6.20	       a() -> n__a()
12.71/6.20	       activate(X) -> X
12.71/6.20	     Qed
12.71/6.20	EOF