YES(?,O(n^2))
24.16/9.13	YES(?,O(n^2))
24.16/9.14	
24.16/9.14	Problem:
24.16/9.14	 f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	 f(X) -> n__f(X)
24.16/9.14	 a() -> n__a()
24.16/9.14	 g(X) -> n__g(X)
24.16/9.14	 activate(n__f(X)) -> f(X)
24.16/9.14	 activate(n__a()) -> a()
24.16/9.14	 activate(n__g(X)) -> g(activate(X))
24.16/9.14	 activate(X) -> X
24.16/9.14	
24.16/9.14	Proof:
24.16/9.14	 Complexity Transformation Processor:
24.16/9.14	  strict:
24.16/9.14	   f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	   f(X) -> n__f(X)
24.16/9.14	   a() -> n__a()
24.16/9.14	   g(X) -> n__g(X)
24.16/9.14	   activate(n__f(X)) -> f(X)
24.16/9.14	   activate(n__a()) -> a()
24.16/9.14	   activate(n__g(X)) -> g(activate(X))
24.16/9.14	   activate(X) -> X
24.16/9.14	  weak:
24.16/9.14	   
24.16/9.14	  Matrix Interpretation Processor: dim=1
24.16/9.14	   
24.16/9.14	   max_matrix:
24.16/9.14	    1
24.16/9.14	   interpretation:
24.16/9.14	    [activate](x0) = x0 + 65,
24.16/9.14	    
24.16/9.14	    [g](x0) = x0 + 191,
24.16/9.14	    
24.16/9.14	    [a] = 0,
24.16/9.14	    
24.16/9.14	    [n__g](x0) = x0 + 124,
24.16/9.14	    
24.16/9.14	    [f](x0) = x0 + 28,
24.16/9.14	    
24.16/9.14	    [n__f](x0) = x0 + 136,
24.16/9.14	    
24.16/9.14	    [n__a] = 160
24.16/9.14	   orientation:
24.16/9.14	    f(n__f(n__a())) = 324 >= 448 = f(n__g(n__f(n__a())))
24.16/9.14	    
24.16/9.14	    f(X) = X + 28 >= X + 136 = n__f(X)
24.16/9.14	    
24.16/9.14	    a() = 0 >= 160 = n__a()
24.16/9.14	    
24.16/9.14	    g(X) = X + 191 >= X + 124 = n__g(X)
24.16/9.14	    
24.16/9.14	    activate(n__f(X)) = X + 201 >= X + 28 = f(X)
24.16/9.14	    
24.16/9.14	    activate(n__a()) = 225 >= 0 = a()
24.16/9.14	    
24.16/9.14	    activate(n__g(X)) = X + 189 >= X + 256 = g(activate(X))
24.16/9.14	    
24.16/9.14	    activate(X) = X + 65 >= X = X
24.16/9.14	   problem:
24.16/9.14	    strict:
24.16/9.14	     f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	     f(X) -> n__f(X)
24.16/9.14	     a() -> n__a()
24.16/9.14	     activate(n__g(X)) -> g(activate(X))
24.16/9.14	    weak:
24.16/9.14	     g(X) -> n__g(X)
24.16/9.14	     activate(n__f(X)) -> f(X)
24.16/9.14	     activate(n__a()) -> a()
24.16/9.14	     activate(X) -> X
24.16/9.14	   Matrix Interpretation Processor: dim=1
24.16/9.14	    
24.16/9.14	    max_matrix:
24.16/9.14	     1
24.16/9.14	    interpretation:
24.16/9.14	     [activate](x0) = x0 + 3,
24.16/9.14	     
24.16/9.14	     [g](x0) = x0 + 232,
24.16/9.14	     
24.16/9.14	     [a] = 0,
24.16/9.14	     
24.16/9.14	     [n__g](x0) = x0 + 128,
24.16/9.14	     
24.16/9.14	     [f](x0) = x0 + 8,
24.16/9.14	     
24.16/9.14	     [n__f](x0) = x0 + 6,
24.16/9.14	     
24.16/9.14	     [n__a] = 128
24.16/9.14	    orientation:
24.16/9.14	     f(n__f(n__a())) = 142 >= 270 = f(n__g(n__f(n__a())))
24.16/9.14	     
24.16/9.14	     f(X) = X + 8 >= X + 6 = n__f(X)
24.16/9.14	     
24.16/9.14	     a() = 0 >= 128 = n__a()
24.16/9.14	     
24.16/9.14	     activate(n__g(X)) = X + 131 >= X + 235 = g(activate(X))
24.16/9.14	     
24.16/9.14	     g(X) = X + 232 >= X + 128 = n__g(X)
24.16/9.14	     
24.16/9.14	     activate(n__f(X)) = X + 9 >= X + 8 = f(X)
24.16/9.14	     
24.16/9.14	     activate(n__a()) = 131 >= 0 = a()
24.16/9.14	     
24.16/9.14	     activate(X) = X + 3 >= X = X
24.16/9.14	    problem:
24.16/9.14	     strict:
24.16/9.14	      f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	      a() -> n__a()
24.16/9.14	      activate(n__g(X)) -> g(activate(X))
24.16/9.14	     weak:
24.16/9.14	      f(X) -> n__f(X)
24.16/9.14	      g(X) -> n__g(X)
24.16/9.14	      activate(n__f(X)) -> f(X)
24.16/9.14	      activate(n__a()) -> a()
24.16/9.14	      activate(X) -> X
24.16/9.14	    Matrix Interpretation Processor: dim=1
24.16/9.14	     
24.16/9.14	     max_matrix:
24.16/9.14	      1
24.16/9.14	     interpretation:
24.16/9.14	      [activate](x0) = x0 + 4,
24.16/9.14	      
24.16/9.14	      [g](x0) = x0 + 118,
24.16/9.14	      
24.16/9.14	      [a] = 17,
24.16/9.14	      
24.16/9.14	      [n__g](x0) = x0 + 112,
24.16/9.14	      
24.16/9.14	      [f](x0) = x0 + 1,
24.16/9.14	      
24.16/9.14	      [n__f](x0) = x0,
24.16/9.14	      
24.16/9.14	      [n__a] = 16
24.16/9.14	     orientation:
24.16/9.14	      f(n__f(n__a())) = 17 >= 129 = f(n__g(n__f(n__a())))
24.16/9.14	      
24.16/9.14	      a() = 17 >= 16 = n__a()
24.16/9.14	      
24.16/9.14	      activate(n__g(X)) = X + 116 >= X + 122 = g(activate(X))
24.16/9.14	      
24.16/9.14	      f(X) = X + 1 >= X = n__f(X)
24.16/9.14	      
24.16/9.14	      g(X) = X + 118 >= X + 112 = n__g(X)
24.16/9.14	      
24.16/9.14	      activate(n__f(X)) = X + 4 >= X + 1 = f(X)
24.16/9.14	      
24.16/9.14	      activate(n__a()) = 20 >= 17 = a()
24.16/9.14	      
24.16/9.14	      activate(X) = X + 4 >= X = X
24.16/9.14	     problem:
24.16/9.14	      strict:
24.16/9.14	       f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	       activate(n__g(X)) -> g(activate(X))
24.16/9.14	      weak:
24.16/9.14	       a() -> n__a()
24.16/9.14	       f(X) -> n__f(X)
24.16/9.14	       g(X) -> n__g(X)
24.16/9.14	       activate(n__f(X)) -> f(X)
24.16/9.14	       activate(n__a()) -> a()
24.16/9.14	       activate(X) -> X
24.16/9.14	     Matrix Interpretation Processor: dim=2
24.16/9.14	      
24.16/9.14	      max_matrix:
24.16/9.14	       [1 1]
24.16/9.14	       [0 1]
24.16/9.14	      interpretation:
24.16/9.14	                        [1 1]  
24.16/9.14	       [activate](x0) = [0 1]x0,
24.16/9.14	       
24.16/9.14	                      [0]
24.16/9.14	       [g](x0) = x0 + [5],
24.16/9.14	       
24.16/9.14	             [0]
24.16/9.14	       [a] = [0],
24.16/9.14	       
24.16/9.14	                         [0]
24.16/9.14	       [n__g](x0) = x0 + [5],
24.16/9.14	       
24.16/9.14	                 [1 0]     [4]
24.16/9.14	       [f](x0) = [0 0]x0 + [0],
24.16/9.14	       
24.16/9.14	                    [1 0]     [4]
24.16/9.14	       [n__f](x0) = [0 0]x0 + [0],
24.16/9.14	       
24.16/9.14	                [0]
24.16/9.14	       [n__a] = [0]
24.16/9.14	      orientation:
24.16/9.14	                         [8]    [8]                        
24.16/9.14	       f(n__f(n__a())) = [0] >= [0] = f(n__g(n__f(n__a())))
24.16/9.14	       
24.16/9.14	                           [1 1]    [5]    [1 1]    [0]                 
24.16/9.14	       activate(n__g(X)) = [0 1]X + [5] >= [0 1]X + [5] = g(activate(X))
24.16/9.14	       
24.16/9.14	             [0]    [0]         
24.16/9.14	       a() = [0] >= [0] = n__a()
24.16/9.14	       
24.16/9.14	              [1 0]    [4]    [1 0]    [4]          
24.16/9.14	       f(X) = [0 0]X + [0] >= [0 0]X + [0] = n__f(X)
24.16/9.14	       
24.16/9.14	                  [0]        [0]          
24.16/9.14	       g(X) = X + [5] >= X + [5] = n__g(X)
24.16/9.14	       
24.16/9.14	                           [1 0]    [4]    [1 0]    [4]       
24.16/9.14	       activate(n__f(X)) = [0 0]X + [0] >= [0 0]X + [0] = f(X)
24.16/9.14	       
24.16/9.14	                          [0]    [0]      
24.16/9.14	       activate(n__a()) = [0] >= [0] = a()
24.16/9.14	       
24.16/9.14	                     [1 1]          
24.16/9.14	       activate(X) = [0 1]X >= X = X
24.16/9.14	      problem:
24.16/9.14	       strict:
24.16/9.14	        f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	       weak:
24.16/9.14	        activate(n__g(X)) -> g(activate(X))
24.16/9.14	        a() -> n__a()
24.16/9.14	        f(X) -> n__f(X)
24.16/9.14	        g(X) -> n__g(X)
24.16/9.14	        activate(n__f(X)) -> f(X)
24.16/9.14	        activate(n__a()) -> a()
24.16/9.14	        activate(X) -> X
24.16/9.14	      Matrix Interpretation Processor: dim=2
24.16/9.14	       
24.16/9.14	       max_matrix:
24.16/9.14	        [1 1]
24.16/9.14	        [0 1]
24.16/9.14	       interpretation:
24.16/9.14	                           
24.16/9.14	        [activate](x0) = x0,
24.16/9.14	        
24.16/9.14	                  [1 0]  
24.16/9.14	        [g](x0) = [0 0]x0,
24.16/9.14	        
24.16/9.14	              [0]
24.16/9.14	        [a] = [0],
24.16/9.14	        
24.16/9.14	                     [1 0]  
24.16/9.14	        [n__g](x0) = [0 0]x0,
24.16/9.14	        
24.16/9.14	                  [1 1]     [0]
24.16/9.14	        [f](x0) = [0 0]x0 + [1],
24.16/9.14	        
24.16/9.14	                     [1 1]     [0]
24.16/9.14	        [n__f](x0) = [0 0]x0 + [1],
24.16/9.14	        
24.16/9.14	                 [0]
24.16/9.14	        [n__a] = [0]
24.16/9.14	       orientation:
24.16/9.14	                          [1]    [0]                        
24.16/9.14	        f(n__f(n__a())) = [1] >= [1] = f(n__g(n__f(n__a())))
24.16/9.14	        
24.16/9.14	                            [1 0]     [1 0]                  
24.16/9.14	        activate(n__g(X)) = [0 0]X >= [0 0]X = g(activate(X))
24.16/9.14	        
24.16/9.14	              [0]    [0]         
24.16/9.14	        a() = [0] >= [0] = n__a()
24.16/9.14	        
24.16/9.14	               [1 1]    [0]    [1 1]    [0]          
24.16/9.14	        f(X) = [0 0]X + [1] >= [0 0]X + [1] = n__f(X)
24.16/9.14	        
24.16/9.14	               [1 0]     [1 0]           
24.16/9.14	        g(X) = [0 0]X >= [0 0]X = n__g(X)
24.16/9.14	        
24.16/9.14	                            [1 1]    [0]    [1 1]    [0]       
24.16/9.14	        activate(n__f(X)) = [0 0]X + [1] >= [0 0]X + [1] = f(X)
24.16/9.14	        
24.16/9.14	                           [0]    [0]      
24.16/9.14	        activate(n__a()) = [0] >= [0] = a()
24.16/9.14	        
24.16/9.14	                                
24.16/9.14	        activate(X) = X >= X = X
24.16/9.14	       problem:
24.16/9.14	        strict:
24.16/9.14	         
24.16/9.14	        weak:
24.16/9.14	         f(n__f(n__a())) -> f(n__g(n__f(n__a())))
24.16/9.14	         activate(n__g(X)) -> g(activate(X))
24.16/9.14	         a() -> n__a()
24.16/9.14	         f(X) -> n__f(X)
24.16/9.14	         g(X) -> n__g(X)
24.16/9.14	         activate(n__f(X)) -> f(X)
24.16/9.14	         activate(n__a()) -> a()
24.16/9.14	         activate(X) -> X
24.16/9.14	       Qed
24.16/9.15	EOF