YES(?,O(n^2))
16.06/8.01	YES(?,O(n^2))
16.06/8.01	
16.06/8.01	Problem:
16.06/8.01	 g(0(),f(x,x)) -> x
16.06/8.01	 g(x,s(y)) -> g(f(x,y),0())
16.06/8.01	 g(s(x),y) -> g(f(x,y),0())
16.06/8.01	 g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.06/8.01	
16.06/8.01	Proof:
16.06/8.01	 Complexity Transformation Processor:
16.06/8.01	  strict:
16.06/8.01	   g(0(),f(x,x)) -> x
16.06/8.01	   g(x,s(y)) -> g(f(x,y),0())
16.06/8.01	   g(s(x),y) -> g(f(x,y),0())
16.06/8.01	   g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.06/8.01	  weak:
16.06/8.01	   
16.06/8.01	  Matrix Interpretation Processor: dim=1
16.06/8.01	   
16.06/8.01	   max_matrix:
16.06/8.01	    1
16.06/8.01	   interpretation:
16.06/8.01	    [s](x0) = x0 + 113,
16.06/8.01	    
16.06/8.01	    [g](x0, x1) = x0 + x1,
16.06/8.01	    
16.06/8.01	    [f](x0, x1) = x0 + x1 + 4,
16.06/8.01	    
16.06/8.01	    [0] = 16
16.06/8.01	   orientation:
16.06/8.01	    g(0(),f(x,x)) = 2x + 20 >= x = x
16.06/8.01	    
16.06/8.01	    g(x,s(y)) = x + y + 113 >= x + y + 20 = g(f(x,y),0())
16.06/8.01	    
16.06/8.01	    g(s(x),y) = x + y + 113 >= x + y + 20 = g(f(x,y),0())
16.06/8.01	    
16.06/8.01	    g(f(x,y),0()) = x + y + 20 >= x + y + 36 = f(g(x,0()),g(y,0()))
16.06/8.01	   problem:
16.06/8.01	    strict:
16.06/8.01	     g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.06/8.01	    weak:
16.06/8.01	     g(0(),f(x,x)) -> x
16.06/8.01	     g(x,s(y)) -> g(f(x,y),0())
16.06/8.01	     g(s(x),y) -> g(f(x,y),0())
16.06/8.01	   Matrix Interpretation Processor: dim=2
16.06/8.01	    
16.06/8.01	    max_matrix:
16.06/8.01	     [1 3]
16.06/8.01	     [0 1]
16.06/8.01	    interpretation:
16.06/8.01	                    [1]
16.06/8.01	     [s](x0) = x0 + [1],
16.06/8.01	     
16.06/8.01	                   [1 2]     [1 3]     [1]
16.06/8.01	     [g](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
16.06/8.01	     
16.06/8.01	                             [0]
16.06/8.01	     [f](x0, x1) = x0 + x1 + [1],
16.06/8.01	     
16.06/8.01	           [0]
16.06/8.01	     [0] = [0]
16.06/8.01	    orientation:
16.06/8.01	                     [1 2]    [1 2]    [3]    [1 2]    [1 2]    [2]                       
16.06/8.01	     g(f(x,y),0()) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = f(g(x,0()),g(y,0()))
16.06/8.01	     
16.06/8.01	                     [2 6]    [4]         
16.06/8.01	     g(0(),f(x,x)) = [0 2]x + [1] >= x = x
16.06/8.01	     
16.06/8.01	                 [1 2]    [1 3]    [5]    [1 2]    [1 2]    [3]                
16.06/8.01	     g(x,s(y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0())
16.06/8.01	     
16.06/8.01	                 [1 2]    [1 3]    [4]    [1 2]    [1 2]    [3]                
16.06/8.01	     g(s(x),y) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0())
16.06/8.01	    problem:
16.06/8.01	     strict:
16.06/8.01	      
16.06/8.01	     weak:
16.06/8.01	      g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.06/8.01	      g(0(),f(x,x)) -> x
16.06/8.01	      g(x,s(y)) -> g(f(x,y),0())
16.06/8.01	      g(s(x),y) -> g(f(x,y),0())
16.06/8.01	    Qed
16.06/8.01	EOF