YES(?,O(n^2))
45.55/19.19	YES(?,O(n^2))
45.65/19.20	
45.65/19.20	Problem:
45.65/19.20	 a__f(f(a())) -> a__f(g(f(a())))
45.65/19.20	 mark(f(X)) -> a__f(mark(X))
45.65/19.20	 mark(a()) -> a()
45.65/19.20	 mark(g(X)) -> g(X)
45.65/19.20	 a__f(X) -> f(X)
45.65/19.20	
45.65/19.20	Proof:
45.65/19.20	 Complexity Transformation Processor:
45.65/19.20	  strict:
45.65/19.20	   a__f(f(a())) -> a__f(g(f(a())))
45.65/19.20	   mark(f(X)) -> a__f(mark(X))
45.65/19.20	   mark(a()) -> a()
45.65/19.20	   mark(g(X)) -> g(X)
45.65/19.20	   a__f(X) -> f(X)
45.65/19.20	  weak:
45.65/19.20	   
45.65/19.20	  Matrix Interpretation Processor: dim=1
45.65/19.20	   
45.65/19.20	   max_matrix:
45.65/19.20	    1
45.65/19.20	   interpretation:
45.65/19.20	    [mark](x0) = x0 + 14,
45.65/19.20	    
45.65/19.20	    [g](x0) = x0 + 6,
45.65/19.20	    
45.65/19.20	    [a__f](x0) = x0 + 7,
45.65/19.20	    
45.65/19.20	    [f](x0) = x0 + 2,
45.65/19.20	    
45.65/19.20	    [a] = 0
45.65/19.20	   orientation:
45.65/19.20	    a__f(f(a())) = 9 >= 15 = a__f(g(f(a())))
45.65/19.20	    
45.65/19.20	    mark(f(X)) = X + 16 >= X + 21 = a__f(mark(X))
45.65/19.20	    
45.65/19.20	    mark(a()) = 14 >= 0 = a()
45.65/19.20	    
45.65/19.20	    mark(g(X)) = X + 20 >= X + 6 = g(X)
45.65/19.20	    
45.65/19.20	    a__f(X) = X + 7 >= X + 2 = f(X)
45.65/19.20	   problem:
45.65/19.20	    strict:
45.65/19.20	     a__f(f(a())) -> a__f(g(f(a())))
45.65/19.20	     mark(f(X)) -> a__f(mark(X))
45.65/19.20	    weak:
45.65/19.20	     mark(a()) -> a()
45.65/19.20	     mark(g(X)) -> g(X)
45.65/19.20	     a__f(X) -> f(X)
45.65/19.20	   Matrix Interpretation Processor: dim=2
45.65/19.20	    
45.65/19.20	    max_matrix:
45.65/19.20	     [1 1]
45.65/19.20	     [0 1]
45.65/19.20	    interpretation:
45.65/19.20	                  [1 1]  
45.65/19.20	     [mark](x0) = [0 1]x0,
45.65/19.20	     
45.65/19.20	                 
45.65/19.20	     [g](x0) = x0,
45.65/19.20	     
45.65/19.20	                       [2]
45.65/19.20	     [a__f](x0) = x0 + [2],
45.65/19.20	     
45.65/19.20	                    [1]
45.65/19.20	     [f](x0) = x0 + [2],
45.65/19.20	     
45.65/19.20	           [7]
45.65/19.20	     [a] = [3]
45.65/19.20	    orientation:
45.65/19.20	                    [10]    [10]                  
45.65/19.20	     a__f(f(a())) = [7 ] >= [7 ] = a__f(g(f(a())))
45.65/19.20	     
45.65/19.20	                  [1 1]    [3]    [1 1]    [2]                
45.65/19.20	     mark(f(X)) = [0 1]X + [2] >= [0 1]X + [2] = a__f(mark(X))
45.65/19.20	     
45.65/19.20	                 [10]    [7]      
45.65/19.20	     mark(a()) = [3 ] >= [3] = a()
45.65/19.20	     
45.65/19.20	                  [1 1]             
45.65/19.20	     mark(g(X)) = [0 1]X >= X = g(X)
45.65/19.20	     
45.65/19.20	                   [2]        [1]       
45.65/19.20	     a__f(X) = X + [2] >= X + [2] = f(X)
45.65/19.20	    problem:
45.65/19.20	     strict:
45.65/19.20	      a__f(f(a())) -> a__f(g(f(a())))
45.65/19.20	     weak:
45.65/19.20	      mark(f(X)) -> a__f(mark(X))
45.65/19.20	      mark(a()) -> a()
45.65/19.20	      mark(g(X)) -> g(X)
45.65/19.20	      a__f(X) -> f(X)
45.65/19.20	    Matrix Interpretation Processor: dim=4
45.65/19.20	     
45.65/19.20	     max_matrix:
45.65/19.20	      [1 0 0 1]
45.65/19.20	      [0 0 0 0]
45.65/19.20	      [0 0 0 0]
45.65/19.20	      [0 0 0 1]
45.65/19.20	     interpretation:
45.65/19.20	                   [1 0 0 0]  
45.65/19.20	                   [0 0 0 0]  
45.65/19.20	      [mark](x0) = [0 0 0 0]x0
45.65/19.20	                   [0 0 0 1]  ,
45.65/19.20	      
45.65/19.20	                [1 0 0 0]  
45.65/19.20	                [0 0 0 0]  
45.65/19.20	      [g](x0) = [0 0 0 0]x0
45.65/19.20	                [0 0 0 0]  ,
45.65/19.20	      
45.65/19.20	                   [1 0 0 1]     [0]
45.65/19.20	                   [0 0 0 0]     [0]
45.65/19.20	      [a__f](x0) = [0 0 0 0]x0 + [0]
45.65/19.20	                   [0 0 0 0]     [1],
45.65/19.20	      
45.65/19.20	                [1 0 0 1]     [0]
45.65/19.20	                [0 0 0 0]     [0]
45.65/19.20	      [f](x0) = [0 0 0 0]x0 + [0]
45.65/19.20	                [0 0 0 0]     [1],
45.65/19.20	      
45.65/19.20	            [0]
45.65/19.20	            [0]
45.65/19.20	      [a] = [0]
45.65/19.20	            [0]
45.65/19.20	     orientation:
45.65/19.20	                     [1]    [0]                  
45.65/19.20	                     [0]    [0]                  
45.65/19.20	      a__f(f(a())) = [0] >= [0] = a__f(g(f(a())))
45.65/19.20	                     [1]    [1]                  
45.65/19.20	      
45.65/19.20	                   [1 0 0 1]    [0]    [1 0 0 1]    [0]                
45.65/19.20	                   [0 0 0 0]    [0]    [0 0 0 0]    [0]                
45.65/19.20	      mark(f(X)) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = a__f(mark(X))
45.65/19.20	                   [0 0 0 0]    [1]    [0 0 0 0]    [1]                
45.65/19.20	      
45.65/19.20	                  [0]    [0]      
45.65/19.20	                  [0]    [0]      
45.65/19.20	      mark(a()) = [0] >= [0] = a()
45.65/19.20	                  [0]    [0]      
45.65/19.20	      
45.65/19.20	                   [1 0 0 0]     [1 0 0 0]        
45.65/19.20	                   [0 0 0 0]     [0 0 0 0]        
45.65/19.20	      mark(g(X)) = [0 0 0 0]X >= [0 0 0 0]X = g(X)
45.65/19.20	                   [0 0 0 0]     [0 0 0 0]        
45.65/19.20	      
45.65/19.20	                [1 0 0 1]    [0]    [1 0 0 1]    [0]       
45.65/19.20	                [0 0 0 0]    [0]    [0 0 0 0]    [0]       
45.65/19.20	      a__f(X) = [0 0 0 0]X + [0] >= [0 0 0 0]X + [0] = f(X)
45.65/19.20	                [0 0 0 0]    [1]    [0 0 0 0]    [1]       
45.65/19.20	     problem:
45.65/19.20	      strict:
45.65/19.20	       
45.65/19.20	      weak:
45.65/19.20	       a__f(f(a())) -> a__f(g(f(a())))
45.65/19.20	       mark(f(X)) -> a__f(mark(X))
45.65/19.20	       mark(a()) -> a()
45.65/19.20	       mark(g(X)) -> g(X)
45.65/19.20	       a__f(X) -> f(X)
45.65/19.20	     Qed
45.65/19.20	EOF