YES(?,O(n^2))
8.91/6.01	YES(?,O(n^2))
8.91/6.01	
8.91/6.01	Problem:
8.91/6.01	 +(0(),y) -> y
8.91/6.01	 +(s(x),y) -> s(+(x,y))
8.91/6.01	 -(0(),y) -> 0()
8.91/6.01	 -(x,0()) -> x
8.91/6.01	 -(s(x),s(y)) -> -(x,y)
8.91/6.01	
8.91/6.01	Proof:
8.91/6.01	 Complexity Transformation Processor:
8.91/6.01	  strict:
8.91/6.01	   +(0(),y) -> y
8.91/6.01	   +(s(x),y) -> s(+(x,y))
8.91/6.01	   -(0(),y) -> 0()
8.91/6.01	   -(x,0()) -> x
8.91/6.01	   -(s(x),s(y)) -> -(x,y)
8.91/6.01	  weak:
8.91/6.01	   
8.91/6.01	  Matrix Interpretation Processor: dim=1
8.91/6.01	   
8.91/6.01	   max_matrix:
8.91/6.01	    1
8.91/6.01	   interpretation:
8.91/6.01	    [-](x0, x1) = x0 + x1 + 70,
8.91/6.01	    
8.91/6.01	    [s](x0) = x0,
8.91/6.01	    
8.91/6.01	    [+](x0, x1) = x0 + x1 + 224,
8.91/6.01	    
8.91/6.01	    [0] = 32
8.91/6.01	   orientation:
8.91/6.01	    +(0(),y) = y + 256 >= y = y
8.91/6.01	    
8.91/6.01	    +(s(x),y) = x + y + 224 >= x + y + 224 = s(+(x,y))
8.91/6.01	    
8.91/6.01	    -(0(),y) = y + 102 >= 32 = 0()
8.91/6.01	    
8.91/6.01	    -(x,0()) = x + 102 >= x = x
8.91/6.01	    
8.91/6.01	    -(s(x),s(y)) = x + y + 70 >= x + y + 70 = -(x,y)
8.91/6.01	   problem:
8.91/6.01	    strict:
8.91/6.01	     +(s(x),y) -> s(+(x,y))
8.91/6.01	     -(s(x),s(y)) -> -(x,y)
8.91/6.01	    weak:
8.91/6.01	     +(0(),y) -> y
8.91/6.01	     -(0(),y) -> 0()
8.91/6.01	     -(x,0()) -> x
8.91/6.01	   Matrix Interpretation Processor: dim=1
8.91/6.01	    
8.91/6.01	    max_matrix:
8.91/6.01	     1
8.91/6.01	    interpretation:
8.91/6.01	     [-](x0, x1) = x0 + x1 + 117,
8.91/6.01	     
8.91/6.01	     [s](x0) = x0 + 135,
8.91/6.01	     
8.91/6.01	     [+](x0, x1) = x0 + x1,
8.91/6.01	     
8.91/6.01	     [0] = 0
8.91/6.01	    orientation:
8.91/6.01	     +(s(x),y) = x + y + 135 >= x + y + 135 = s(+(x,y))
8.91/6.01	     
8.91/6.01	     -(s(x),s(y)) = x + y + 387 >= x + y + 117 = -(x,y)
8.91/6.01	     
8.91/6.01	     +(0(),y) = y >= y = y
8.91/6.01	     
8.91/6.01	     -(0(),y) = y + 117 >= 0 = 0()
8.91/6.01	     
8.91/6.01	     -(x,0()) = x + 117 >= x = x
8.91/6.01	    problem:
8.91/6.01	     strict:
8.91/6.01	      +(s(x),y) -> s(+(x,y))
8.91/6.01	     weak:
8.91/6.01	      -(s(x),s(y)) -> -(x,y)
8.91/6.01	      +(0(),y) -> y
8.91/6.01	      -(0(),y) -> 0()
8.91/6.01	      -(x,0()) -> x
8.91/6.01	    Matrix Interpretation Processor: dim=2
8.91/6.01	     
8.91/6.01	     max_matrix:
8.91/6.01	      [1 1]
8.91/6.01	      [0 1]
8.91/6.01	     interpretation:
8.91/6.01	                    [1 1]     [1 1]     [7]
8.91/6.01	      [-](x0, x1) = [0 1]x0 + [0 1]x1 + [2],
8.91/6.01	      
8.91/6.01	                     [0]
8.91/6.01	      [s](x0) = x0 + [1],
8.91/6.01	      
8.91/6.01	                    [1 1]     [1 1]     [0]
8.91/6.01	      [+](x0, x1) = [0 1]x0 + [0 1]x1 + [2],
8.91/6.01	      
8.91/6.01	            [6]
8.91/6.01	      [0] = [2]
8.91/6.01	     orientation:
8.91/6.01	                  [1 1]    [1 1]    [1]    [1 1]    [1 1]    [0]            
8.91/6.01	      +(s(x),y) = [0 1]x + [0 1]y + [3] >= [0 1]x + [0 1]y + [3] = s(+(x,y))
8.91/6.01	      
8.91/6.01	                     [1 1]    [1 1]    [9]    [1 1]    [1 1]    [7]         
8.91/6.01	      -(s(x),s(y)) = [0 1]x + [0 1]y + [4] >= [0 1]x + [0 1]y + [2] = -(x,y)
8.91/6.01	      
8.91/6.01	                 [1 1]    [8]         
8.91/6.01	      +(0(),y) = [0 1]y + [4] >= y = y
8.91/6.01	      
8.91/6.01	                 [1 1]    [15]    [6]      
8.91/6.01	      -(0(),y) = [0 1]y + [4 ] >= [2] = 0()
8.91/6.01	      
8.91/6.01	                 [1 1]    [15]         
8.91/6.01	      -(x,0()) = [0 1]x + [4 ] >= x = x
8.91/6.01	     problem:
8.91/6.01	      strict:
8.91/6.01	       
8.91/6.01	      weak:
8.91/6.01	       +(s(x),y) -> s(+(x,y))
8.91/6.01	       -(s(x),s(y)) -> -(x,y)
8.91/6.01	       +(0(),y) -> y
8.91/6.01	       -(0(),y) -> 0()
8.91/6.01	       -(x,0()) -> x
8.91/6.01	     Qed
8.91/6.02	EOF