YES(?,O(n^2))
16.31/8.43	YES(?,O(n^2))
16.31/8.43	
16.31/8.43	Problem:
16.31/8.43	 +(0(),y) -> y
16.31/8.43	 +(s(x),y) -> s(+(x,y))
16.31/8.43	 +(s(x),y) -> +(x,s(y))
16.31/8.43	
16.31/8.43	Proof:
16.31/8.43	 Complexity Transformation Processor:
16.31/8.43	  strict:
16.31/8.43	   +(0(),y) -> y
16.31/8.43	   +(s(x),y) -> s(+(x,y))
16.31/8.43	   +(s(x),y) -> +(x,s(y))
16.31/8.43	  weak:
16.31/8.43	   
16.31/8.43	  Matrix Interpretation Processor: dim=1
16.31/8.43	   
16.31/8.43	   max_matrix:
16.31/8.43	    1
16.31/8.43	   interpretation:
16.31/8.43	    [s](x0) = x0,
16.31/8.43	    
16.31/8.43	    [+](x0, x1) = x0 + x1 + 177,
16.31/8.43	    
16.31/8.43	    [0] = 0
16.31/8.43	   orientation:
16.31/8.43	    +(0(),y) = y + 177 >= y = y
16.31/8.43	    
16.31/8.43	    +(s(x),y) = x + y + 177 >= x + y + 177 = s(+(x,y))
16.31/8.43	    
16.31/8.43	    +(s(x),y) = x + y + 177 >= x + y + 177 = +(x,s(y))
16.31/8.43	   problem:
16.31/8.43	    strict:
16.31/8.43	     +(s(x),y) -> s(+(x,y))
16.31/8.43	     +(s(x),y) -> +(x,s(y))
16.31/8.43	    weak:
16.31/8.43	     +(0(),y) -> y
16.31/8.43	   Splitting Processor:
16.31/8.43	    strict:
16.31/8.43	     +(s(x),y) -> s(+(x,y))
16.31/8.43	    weak:
16.31/8.43	     +(0(),y) -> y
16.31/8.43	     +(s(x),y) -> +(x,s(y))
16.31/8.43	    Matrix Interpretation Processor: dim=2
16.31/8.43	     
16.31/8.43	     max_matrix:
16.31/8.43	      [1 1]
16.31/8.43	      [0 1]
16.31/8.43	     interpretation:
16.31/8.43	                     [2]
16.31/8.43	      [s](x0) = x0 + [1],
16.31/8.43	      
16.31/8.43	                    [1 1]       
16.31/8.43	      [+](x0, x1) = [0 1]x0 + x1,
16.31/8.43	      
16.31/8.43	            [0]
16.31/8.43	      [0] = [0]
16.31/8.43	     orientation:
16.31/8.43	                  [1 1]        [3]    [1 1]        [2]            
16.31/8.43	      +(s(x),y) = [0 1]x + y + [1] >= [0 1]x + y + [1] = +(x,s(y))
16.31/8.43	      
16.31/8.43	                  [1 1]        [3]    [1 1]        [2]            
16.31/8.43	      +(s(x),y) = [0 1]x + y + [1] >= [0 1]x + y + [1] = s(+(x,y))
16.31/8.43	      
16.31/8.43	                           
16.31/8.43	      +(0(),y) = y >= y = y
16.31/8.43	     problem:
16.31/8.43	      strict:
16.31/8.43	       
16.31/8.43	      weak:
16.31/8.43	       +(s(x),y) -> +(x,s(y))
16.31/8.43	       +(s(x),y) -> s(+(x,y))
16.31/8.43	       +(0(),y) -> y
16.31/8.43	     Qed
16.31/8.43	    
16.31/8.43	    strict:
16.31/8.43	     +(s(x),y) -> +(x,s(y))
16.31/8.43	    weak:
16.31/8.43	     +(s(x),y) -> s(+(x,y))
16.31/8.43	     +(0(),y) -> y
16.31/8.43	    Matrix Interpretation Processor: dim=2
16.31/8.43	     
16.31/8.43	     max_matrix:
16.31/8.43	      [1 3]
16.31/8.43	      [0 1]
16.31/8.43	     interpretation:
16.31/8.43	                     [0]
16.31/8.43	      [s](x0) = x0 + [3],
16.31/8.43	      
16.31/8.43	                    [1 3]     [1 2]     [0]
16.31/8.43	      [+](x0, x1) = [0 1]x0 + [0 1]x1 + [1],
16.31/8.43	      
16.31/8.43	            [3]
16.31/8.43	      [0] = [0]
16.31/8.43	     orientation:
16.31/8.43	                  [1 3]    [1 2]    [9]    [1 3]    [1 2]    [0]            
16.31/8.43	      +(s(x),y) = [0 1]x + [0 1]y + [4] >= [0 1]x + [0 1]y + [4] = s(+(x,y))
16.31/8.43	      
16.31/8.43	                 [1 2]    [3]         
16.31/8.43	      +(0(),y) = [0 1]y + [1] >= y = y
16.31/8.43	      
16.31/8.43	                  [1 3]    [1 2]    [9]    [1 3]    [1 2]    [6]            
16.31/8.43	      +(s(x),y) = [0 1]x + [0 1]y + [4] >= [0 1]x + [0 1]y + [4] = +(x,s(y))
16.31/8.43	     problem:
16.31/8.43	      strict:
16.31/8.43	       
16.31/8.43	      weak:
16.31/8.43	       +(s(x),y) -> s(+(x,y))
16.31/8.43	       +(0(),y) -> y
16.31/8.43	       +(s(x),y) -> +(x,s(y))
16.31/8.43	     Qed
16.31/8.44	EOF