YES(?,O(n^2))
16.19/8.06	YES(?,O(n^2))
16.19/8.06	
16.19/8.06	Problem:
16.19/8.06	 g(0(),f(x,x)) -> x
16.19/8.06	 g(x,s(y)) -> g(f(x,y),0())
16.19/8.06	 g(s(x),y) -> g(f(x,y),0())
16.19/8.06	 g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.19/8.06	
16.19/8.06	Proof:
16.19/8.06	 Complexity Transformation Processor:
16.19/8.06	  strict:
16.19/8.06	   g(0(),f(x,x)) -> x
16.19/8.06	   g(x,s(y)) -> g(f(x,y),0())
16.19/8.06	   g(s(x),y) -> g(f(x,y),0())
16.19/8.06	   g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.19/8.06	  weak:
16.19/8.06	   
16.19/8.06	  Matrix Interpretation Processor: dim=1
16.19/8.06	   
16.19/8.06	   max_matrix:
16.19/8.06	    1
16.19/8.06	   interpretation:
16.19/8.06	    [s](x0) = x0 + 113,
16.19/8.06	    
16.19/8.06	    [g](x0, x1) = x0 + x1,
16.19/8.06	    
16.19/8.06	    [f](x0, x1) = x0 + x1 + 4,
16.19/8.06	    
16.19/8.06	    [0] = 16
16.19/8.06	   orientation:
16.19/8.06	    g(0(),f(x,x)) = 2x + 20 >= x = x
16.19/8.06	    
16.19/8.06	    g(x,s(y)) = x + y + 113 >= x + y + 20 = g(f(x,y),0())
16.19/8.06	    
16.19/8.06	    g(s(x),y) = x + y + 113 >= x + y + 20 = g(f(x,y),0())
16.19/8.06	    
16.19/8.06	    g(f(x,y),0()) = x + y + 20 >= x + y + 36 = f(g(x,0()),g(y,0()))
16.19/8.06	   problem:
16.19/8.06	    strict:
16.19/8.06	     g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.19/8.06	    weak:
16.19/8.06	     g(0(),f(x,x)) -> x
16.19/8.06	     g(x,s(y)) -> g(f(x,y),0())
16.19/8.06	     g(s(x),y) -> g(f(x,y),0())
16.19/8.06	   Matrix Interpretation Processor: dim=2
16.19/8.06	    
16.19/8.06	    max_matrix:
16.19/8.06	     [1 3]
16.19/8.06	     [0 1]
16.19/8.06	    interpretation:
16.19/8.06	                    [1]
16.19/8.06	     [s](x0) = x0 + [1],
16.19/8.06	     
16.19/8.06	                   [1 2]     [1 3]     [1]
16.19/8.06	     [g](x0, x1) = [0 1]x0 + [0 1]x1 + [0],
16.19/8.06	     
16.19/8.06	                             [0]
16.19/8.06	     [f](x0, x1) = x0 + x1 + [1],
16.19/8.06	     
16.19/8.06	           [0]
16.19/8.06	     [0] = [0]
16.19/8.06	    orientation:
16.19/8.06	                     [1 2]    [1 2]    [3]    [1 2]    [1 2]    [2]                       
16.19/8.06	     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.19/8.06	     
16.19/8.06	                     [2 6]    [4]         
16.19/8.06	     g(0(),f(x,x)) = [0 2]x + [1] >= x = x
16.19/8.06	     
16.19/8.06	                 [1 2]    [1 3]    [5]    [1 2]    [1 2]    [3]                
16.19/8.06	     g(x,s(y)) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0())
16.19/8.06	     
16.19/8.06	                 [1 2]    [1 3]    [4]    [1 2]    [1 2]    [3]                
16.19/8.06	     g(s(x),y) = [0 1]x + [0 1]y + [1] >= [0 1]x + [0 1]y + [1] = g(f(x,y),0())
16.19/8.06	    problem:
16.19/8.06	     strict:
16.19/8.06	      
16.19/8.06	     weak:
16.19/8.06	      g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
16.19/8.06	      g(0(),f(x,x)) -> x
16.19/8.06	      g(x,s(y)) -> g(f(x,y),0())
16.19/8.06	      g(s(x),y) -> g(f(x,y),0())
16.19/8.06	    Qed
16.19/8.07	EOF