YES(?,O(n^2))
8.66/5.99	YES(?,O(n^2))
8.66/5.99	
8.66/5.99	Problem:
8.66/5.99	 +(0(),y) -> y
8.66/5.99	 +(s(x),0()) -> s(x)
8.66/5.99	 +(s(x),s(y)) -> s(+(s(x),+(y,0())))
8.66/5.99	
8.66/5.99	Proof:
8.66/5.99	 Complexity Transformation Processor:
8.66/5.99	  strict:
8.66/5.99	   +(0(),y) -> y
8.66/5.99	   +(s(x),0()) -> s(x)
8.66/5.99	   +(s(x),s(y)) -> s(+(s(x),+(y,0())))
8.66/5.99	  weak:
8.66/5.99	   
8.66/5.99	  Matrix Interpretation Processor: dim=1
8.66/5.99	   
8.66/5.99	   max_matrix:
8.66/5.99	    1
8.66/5.99	   interpretation:
8.66/5.99	    [s](x0) = x0 + 1,
8.66/5.99	    
8.66/5.99	    [+](x0, x1) = x0 + x1,
8.66/5.99	    
8.66/5.99	    [0] = 13
8.66/5.99	   orientation:
8.66/5.99	    +(0(),y) = y + 13 >= y = y
8.66/5.99	    
8.66/5.99	    +(s(x),0()) = x + 14 >= x + 1 = s(x)
8.66/5.99	    
8.66/5.99	    +(s(x),s(y)) = x + y + 2 >= x + y + 15 = s(+(s(x),+(y,0())))
8.66/5.99	   problem:
8.66/5.99	    strict:
8.66/5.99	     +(s(x),s(y)) -> s(+(s(x),+(y,0())))
8.66/5.99	    weak:
8.66/5.99	     +(0(),y) -> y
8.66/5.99	     +(s(x),0()) -> s(x)
8.66/5.99	   Matrix Interpretation Processor: dim=2
8.66/5.99	    
8.66/5.99	    max_matrix:
8.66/5.99	     [1 1]
8.66/5.99	     [0 1]
8.66/5.99	    interpretation:
8.66/5.99	                    [0]
8.66/5.99	     [s](x0) = x0 + [1],
8.66/5.99	     
8.66/5.99	                        [1 1]  
8.66/5.99	     [+](x0, x1) = x0 + [0 1]x1,
8.66/5.99	     
8.66/5.99	           [0]
8.66/5.99	     [0] = [0]
8.66/5.99	    orientation:
8.66/5.99	                        [1 1]    [1]        [1 1]    [0]                      
8.66/5.99	     +(s(x),s(y)) = x + [0 1]y + [2] >= x + [0 1]y + [2] = s(+(s(x),+(y,0())))
8.66/5.99	     
8.66/5.99	                [1 1]          
8.66/5.99	     +(0(),y) = [0 1]y >= y = y
8.66/5.99	     
8.66/5.99	                       [0]        [0]       
8.66/5.99	     +(s(x),0()) = x + [1] >= x + [1] = s(x)
8.66/5.99	    problem:
8.66/5.99	     strict:
8.66/5.99	      
8.66/5.99	     weak:
8.66/5.99	      +(s(x),s(y)) -> s(+(s(x),+(y,0())))
8.66/5.99	      +(0(),y) -> y
8.66/5.99	      +(s(x),0()) -> s(x)
8.66/5.99	    Qed
8.81/6.00	EOF