YES(?,O(n^2))
49.25/22.43	YES(?,O(n^2))
49.25/22.44	
49.25/22.44	Problem:
49.25/22.44	 a__f(X) -> g(h(f(X)))
49.25/22.44	 mark(f(X)) -> a__f(mark(X))
49.25/22.44	 mark(g(X)) -> g(X)
49.25/22.44	 mark(h(X)) -> h(mark(X))
49.25/22.44	 a__f(X) -> f(X)
49.25/22.44	
49.25/22.44	Proof:
49.25/22.44	 Complexity Transformation Processor:
49.25/22.44	  strict:
49.25/22.44	   a__f(X) -> g(h(f(X)))
49.25/22.44	   mark(f(X)) -> a__f(mark(X))
49.25/22.44	   mark(g(X)) -> g(X)
49.25/22.44	   mark(h(X)) -> h(mark(X))
49.25/22.44	   a__f(X) -> f(X)
49.25/22.44	  weak:
49.25/22.44	   
49.25/22.44	  Matrix Interpretation Processor: dim=1
49.25/22.44	   
49.25/22.44	   max_matrix:
49.25/22.44	    1
49.25/22.44	   interpretation:
49.25/22.44	    [mark](x0) = x0 + 91,
49.25/22.44	    
49.25/22.44	    [g](x0) = x0 + 129,
49.25/22.44	    
49.25/22.44	    [h](x0) = x0 + 189,
49.25/22.44	    
49.25/22.44	    [f](x0) = x0 + 6,
49.25/22.44	    
49.25/22.44	    [a__f](x0) = x0 + 231
49.25/22.44	   orientation:
49.25/22.44	    a__f(X) = X + 231 >= X + 324 = g(h(f(X)))
49.25/22.44	    
49.25/22.44	    mark(f(X)) = X + 97 >= X + 322 = a__f(mark(X))
49.25/22.44	    
49.25/22.44	    mark(g(X)) = X + 220 >= X + 129 = g(X)
49.25/22.44	    
49.25/22.44	    mark(h(X)) = X + 280 >= X + 280 = h(mark(X))
49.25/22.44	    
49.25/22.44	    a__f(X) = X + 231 >= X + 6 = f(X)
49.25/22.44	   problem:
49.25/22.44	    strict:
49.25/22.44	     a__f(X) -> g(h(f(X)))
49.25/22.44	     mark(f(X)) -> a__f(mark(X))
49.25/22.44	     mark(h(X)) -> h(mark(X))
49.25/22.44	    weak:
49.25/22.44	     mark(g(X)) -> g(X)
49.25/22.44	     a__f(X) -> f(X)
49.25/22.44	   Matrix Interpretation Processor: dim=1
49.25/22.44	    
49.25/22.44	    max_matrix:
49.25/22.44	     1
49.25/22.44	    interpretation:
49.25/22.44	     [mark](x0) = x0 + 193,
49.25/22.44	     
49.25/22.44	     [g](x0) = x0 + 15,
49.25/22.44	     
49.25/22.44	     [h](x0) = x0 + 128,
49.25/22.44	     
49.25/22.44	     [f](x0) = x0,
49.25/22.44	     
49.25/22.44	     [a__f](x0) = x0 + 195
49.25/22.44	    orientation:
49.25/22.44	     a__f(X) = X + 195 >= X + 143 = g(h(f(X)))
49.25/22.44	     
49.25/22.44	     mark(f(X)) = X + 193 >= X + 388 = a__f(mark(X))
49.25/22.44	     
49.25/22.44	     mark(h(X)) = X + 321 >= X + 321 = h(mark(X))
49.25/22.44	     
49.25/22.44	     mark(g(X)) = X + 208 >= X + 15 = g(X)
49.25/22.44	     
49.25/22.44	     a__f(X) = X + 195 >= X = f(X)
49.25/22.44	    problem:
49.25/22.44	     strict:
49.25/22.44	      mark(f(X)) -> a__f(mark(X))
49.25/22.44	      mark(h(X)) -> h(mark(X))
49.25/22.44	     weak:
49.25/22.44	      a__f(X) -> g(h(f(X)))
49.25/22.44	      mark(g(X)) -> g(X)
49.25/22.44	      a__f(X) -> f(X)
49.25/22.44	    Matrix Interpretation Processor: dim=2
49.25/22.44	     
49.25/22.44	     max_matrix:
49.25/22.44	      [1 4]
49.25/22.44	      [0 1]
49.25/22.44	     interpretation:
49.25/22.44	                   [1 1]  
49.25/22.44	      [mark](x0) = [0 1]x0,
49.25/22.44	      
49.25/22.44	                [1 0]  
49.25/22.44	      [g](x0) = [0 0]x0,
49.25/22.44	      
49.25/22.44	                     [0]
49.25/22.44	      [h](x0) = x0 + [2],
49.25/22.44	      
49.25/22.44	                [1 4]  
49.25/22.44	      [f](x0) = [0 1]x0,
49.25/22.44	      
49.25/22.44	                   [1 4]  
49.25/22.44	      [a__f](x0) = [0 1]x0
49.25/22.44	     orientation:
49.25/22.44	                   [1 5]     [1 5]                 
49.25/22.44	      mark(f(X)) = [0 1]X >= [0 1]X = a__f(mark(X))
49.25/22.44	      
49.25/22.44	                   [1 1]    [2]    [1 1]    [0]             
49.25/22.44	      mark(h(X)) = [0 1]X + [2] >= [0 1]X + [2] = h(mark(X))
49.25/22.44	      
49.25/22.44	                [1 4]     [1 4]              
49.25/22.44	      a__f(X) = [0 1]X >= [0 0]X = g(h(f(X)))
49.25/22.44	      
49.25/22.44	                   [1 0]     [1 0]        
49.25/22.44	      mark(g(X)) = [0 0]X >= [0 0]X = g(X)
49.25/22.44	      
49.25/22.44	                [1 4]     [1 4]        
49.25/22.44	      a__f(X) = [0 1]X >= [0 1]X = f(X)
49.25/22.44	     problem:
49.25/22.44	      strict:
49.25/22.44	       mark(f(X)) -> a__f(mark(X))
49.25/22.44	      weak:
49.25/22.44	       mark(h(X)) -> h(mark(X))
49.25/22.44	       a__f(X) -> g(h(f(X)))
49.25/22.44	       mark(g(X)) -> g(X)
49.25/22.44	       a__f(X) -> f(X)
49.25/22.44	     Matrix Interpretation Processor: dim=2
49.25/22.44	      
49.25/22.44	      max_matrix:
49.25/22.44	       [1 1]
49.25/22.44	       [0 1]
49.25/22.44	      interpretation:
49.25/22.44	                    [1 1]  
49.25/22.44	       [mark](x0) = [0 1]x0,
49.25/22.44	       
49.25/22.44	                 [1 0]     [0]
49.25/22.44	       [g](x0) = [0 0]x0 + [2],
49.25/22.44	       
49.25/22.44	                   
49.25/22.44	       [h](x0) = x0,
49.25/22.44	       
49.25/22.44	                      [0]
49.25/22.44	       [f](x0) = x0 + [2],
49.25/22.44	       
49.25/22.44	                         [0]
49.25/22.44	       [a__f](x0) = x0 + [2]
49.25/22.44	      orientation:
49.25/22.44	                    [1 1]    [2]    [1 1]    [0]                
49.25/22.44	       mark(f(X)) = [0 1]X + [2] >= [0 1]X + [2] = a__f(mark(X))
49.25/22.44	       
49.25/22.44	                    [1 1]     [1 1]              
49.25/22.44	       mark(h(X)) = [0 1]X >= [0 1]X = h(mark(X))
49.25/22.44	       
49.25/22.44	                     [0]    [1 0]    [0]             
49.25/22.44	       a__f(X) = X + [2] >= [0 0]X + [2] = g(h(f(X)))
49.25/22.44	       
49.25/22.44	                    [1 0]    [2]    [1 0]    [0]       
49.25/22.44	       mark(g(X)) = [0 0]X + [2] >= [0 0]X + [2] = g(X)
49.25/22.44	       
49.25/22.44	                     [0]        [0]       
49.25/22.44	       a__f(X) = X + [2] >= X + [2] = f(X)
49.25/22.44	      problem:
49.25/22.44	       strict:
49.25/22.44	        
49.25/22.44	       weak:
49.25/22.44	        mark(f(X)) -> a__f(mark(X))
49.25/22.44	        mark(h(X)) -> h(mark(X))
49.25/22.44	        a__f(X) -> g(h(f(X)))
49.25/22.44	        mark(g(X)) -> g(X)
49.25/22.44	        a__f(X) -> f(X)
49.25/22.44	      Qed
49.25/22.44	EOF