YES(O(1),O(n^2))
17.31/6.07	YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	We add the following weak dependency pairs:
17.31/6.07	
17.31/6.07	Strict DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	
17.31/6.07	and mark the set of starting terms.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	We estimate the number of application of {1} by applications of
17.31/6.07	Pre({1}) = {3}. Here rules are labeled as follows:
17.31/6.07	
17.31/6.07	  DPs:
17.31/6.07	    { 1: sum^#(0()) -> c_1()
17.31/6.07	    , 2: sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	    , 3: +^#(x, 0()) -> c_3(x)
17.31/6.07	    , 4: +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict DPs:
17.31/6.07	  { sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Weak DPs: { sum^#(0()) -> c_1() }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	The weightgap principle applies (using the following nonconstant
17.31/6.07	growth matrix-interpretation)
17.31/6.07	
17.31/6.07	The following argument positions are usable:
17.31/6.07	  Uargs(s) = {1}, Uargs(+) = {1}, Uargs(c_2) = {1}, Uargs(+^#) = {1},
17.31/6.07	  Uargs(c_3) = {1}, Uargs(c_4) = {1}
17.31/6.07	
17.31/6.07	TcT has computed the following matrix interpretation satisfying
17.31/6.07	not(EDA) and not(IDA(1)).
17.31/6.07	
17.31/6.07	      [sum](x1) = [0]         
17.31/6.07	                              
17.31/6.07	            [0] = [5]         
17.31/6.07	                              
17.31/6.07	        [s](x1) = [1] x1 + [0]
17.31/6.07	                              
17.31/6.07	    [+](x1, x2) = [1] x1 + [0]
17.31/6.07	                              
17.31/6.07	    [sum^#](x1) = [1] x1 + [7]
17.31/6.07	                              
17.31/6.07	          [c_1] = [4]         
17.31/6.07	                              
17.31/6.07	      [c_2](x1) = [1] x1 + [3]
17.31/6.07	                              
17.31/6.07	  [+^#](x1, x2) = [1] x1 + [0]
17.31/6.07	                              
17.31/6.07	      [c_3](x1) = [1] x1 + [7]
17.31/6.07	                              
17.31/6.07	      [c_4](x1) = [1] x1 + [7]
17.31/6.07	
17.31/6.07	The order satisfies the following ordering constraints:
17.31/6.07	
17.31/6.07	      [sum(0())] =  [0]                     
17.31/6.07	                 ?  [5]                     
17.31/6.07	                 =  [0()]                   
17.31/6.07	                                            
17.31/6.07	     [sum(s(x))] =  [0]                     
17.31/6.07	                 >= [0]                     
17.31/6.07	                 =  [+(sum(x), s(x))]       
17.31/6.07	                                            
17.31/6.07	     [+(x, 0())] =  [1] x + [0]             
17.31/6.07	                 >= [1] x + [0]             
17.31/6.07	                 =  [x]                     
17.31/6.07	                                            
17.31/6.07	    [+(x, s(y))] =  [1] x + [0]             
17.31/6.07	                 >= [1] x + [0]             
17.31/6.07	                 =  [s(+(x, y))]            
17.31/6.07	                                            
17.31/6.07	    [sum^#(0())] =  [12]                    
17.31/6.07	                 >  [4]                     
17.31/6.07	                 =  [c_1()]                 
17.31/6.07	                                            
17.31/6.07	   [sum^#(s(x))] =  [1] x + [7]             
17.31/6.07	                 >  [3]                     
17.31/6.07	                 =  [c_2(+^#(sum(x), s(x)))]
17.31/6.07	                                            
17.31/6.07	   [+^#(x, 0())] =  [1] x + [0]             
17.31/6.07	                 ?  [1] x + [7]             
17.31/6.07	                 =  [c_3(x)]                
17.31/6.07	                                            
17.31/6.07	  [+^#(x, s(y))] =  [1] x + [0]             
17.31/6.07	                 ?  [1] x + [7]             
17.31/6.07	                 =  [c_4(+^#(x, y))]        
17.31/6.07	                                            
17.31/6.07	
17.31/6.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict DPs:
17.31/6.07	  { +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Weak DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x))) }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	The weightgap principle applies (using the following nonconstant
17.31/6.07	growth matrix-interpretation)
17.31/6.07	
17.31/6.07	The following argument positions are usable:
17.31/6.07	  Uargs(s) = {1}, Uargs(+) = {1}, Uargs(c_2) = {1}, Uargs(+^#) = {1},
17.31/6.07	  Uargs(c_3) = {1}, Uargs(c_4) = {1}
17.31/6.07	
17.31/6.07	TcT has computed the following matrix interpretation satisfying
17.31/6.07	not(EDA) and not(IDA(1)).
17.31/6.07	
17.31/6.07	      [sum](x1) = [0]                  
17.31/6.07	                                       
17.31/6.07	            [0] = [1]                  
17.31/6.07	                                       
17.31/6.07	        [s](x1) = [1] x1 + [0]         
17.31/6.07	                                       
17.31/6.07	    [+](x1, x2) = [1] x1 + [0]         
17.31/6.07	                                       
17.31/6.07	    [sum^#](x1) = [1] x1 + [7]         
17.31/6.07	                                       
17.31/6.07	          [c_1] = [0]                  
17.31/6.07	                                       
17.31/6.07	      [c_2](x1) = [1] x1 + [3]         
17.31/6.07	                                       
17.31/6.07	  [+^#](x1, x2) = [1] x1 + [1] x2 + [0]
17.31/6.07	                                       
17.31/6.07	      [c_3](x1) = [1] x1 + [0]         
17.31/6.07	                                       
17.31/6.07	      [c_4](x1) = [1] x1 + [7]         
17.31/6.07	
17.31/6.07	The order satisfies the following ordering constraints:
17.31/6.07	
17.31/6.07	      [sum(0())] =  [0]                     
17.31/6.07	                 ?  [1]                     
17.31/6.07	                 =  [0()]                   
17.31/6.07	                                            
17.31/6.07	     [sum(s(x))] =  [0]                     
17.31/6.07	                 >= [0]                     
17.31/6.07	                 =  [+(sum(x), s(x))]       
17.31/6.07	                                            
17.31/6.07	     [+(x, 0())] =  [1] x + [0]             
17.31/6.07	                 >= [1] x + [0]             
17.31/6.07	                 =  [x]                     
17.31/6.07	                                            
17.31/6.07	    [+(x, s(y))] =  [1] x + [0]             
17.31/6.07	                 >= [1] x + [0]             
17.31/6.07	                 =  [s(+(x, y))]            
17.31/6.07	                                            
17.31/6.07	    [sum^#(0())] =  [8]                     
17.31/6.07	                 >  [0]                     
17.31/6.07	                 =  [c_1()]                 
17.31/6.07	                                            
17.31/6.07	   [sum^#(s(x))] =  [1] x + [7]             
17.31/6.07	                 >  [1] x + [3]             
17.31/6.07	                 =  [c_2(+^#(sum(x), s(x)))]
17.31/6.07	                                            
17.31/6.07	   [+^#(x, 0())] =  [1] x + [1]             
17.31/6.07	                 >  [1] x + [0]             
17.31/6.07	                 =  [c_3(x)]                
17.31/6.07	                                            
17.31/6.07	  [+^#(x, s(y))] =  [1] x + [1] y + [0]     
17.31/6.07	                 ?  [1] x + [1] y + [7]     
17.31/6.07	                 =  [c_4(+^#(x, y))]        
17.31/6.07	                                            
17.31/6.07	
17.31/6.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict DPs: { +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Weak DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x) }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	The weightgap principle applies (using the following nonconstant
17.31/6.07	growth matrix-interpretation)
17.31/6.07	
17.31/6.07	The following argument positions are usable:
17.31/6.07	  Uargs(s) = {1}, Uargs(+) = {1}, Uargs(c_2) = {1}, Uargs(+^#) = {1},
17.31/6.07	  Uargs(c_3) = {1}, Uargs(c_4) = {1}
17.31/6.07	
17.31/6.07	TcT has computed the following matrix interpretation satisfying
17.31/6.07	not(EDA) and not(IDA(1)).
17.31/6.07	
17.31/6.07	      [sum](x1) = [3]                  
17.31/6.07	                                       
17.31/6.07	            [0] = [5]                  
17.31/6.07	                                       
17.31/6.07	        [s](x1) = [1] x1 + [7]         
17.31/6.07	                                       
17.31/6.07	    [+](x1, x2) = [1] x1 + [7]         
17.31/6.07	                                       
17.31/6.07	    [sum^#](x1) = [1] x1 + [7]         
17.31/6.07	                                       
17.31/6.07	          [c_1] = [4]                  
17.31/6.07	                                       
17.31/6.07	      [c_2](x1) = [1] x1 + [1]         
17.31/6.07	                                       
17.31/6.07	  [+^#](x1, x2) = [1] x1 + [1] x2 + [3]
17.31/6.07	                                       
17.31/6.07	      [c_3](x1) = [1] x1 + [0]         
17.31/6.07	                                       
17.31/6.07	      [c_4](x1) = [1] x1 + [5]         
17.31/6.07	
17.31/6.07	The order satisfies the following ordering constraints:
17.31/6.07	
17.31/6.07	      [sum(0())] =  [3]                     
17.31/6.07	                 ?  [5]                     
17.31/6.07	                 =  [0()]                   
17.31/6.07	                                            
17.31/6.07	     [sum(s(x))] =  [3]                     
17.31/6.07	                 ?  [10]                    
17.31/6.07	                 =  [+(sum(x), s(x))]       
17.31/6.07	                                            
17.31/6.07	     [+(x, 0())] =  [1] x + [7]             
17.31/6.07	                 >  [1] x + [0]             
17.31/6.07	                 =  [x]                     
17.31/6.07	                                            
17.31/6.07	    [+(x, s(y))] =  [1] x + [7]             
17.31/6.07	                 ?  [1] x + [14]            
17.31/6.07	                 =  [s(+(x, y))]            
17.31/6.07	                                            
17.31/6.07	    [sum^#(0())] =  [12]                    
17.31/6.07	                 >  [4]                     
17.31/6.07	                 =  [c_1()]                 
17.31/6.07	                                            
17.31/6.07	   [sum^#(s(x))] =  [1] x + [14]            
17.31/6.07	                 >= [1] x + [14]            
17.31/6.07	                 =  [c_2(+^#(sum(x), s(x)))]
17.31/6.07	                                            
17.31/6.07	   [+^#(x, 0())] =  [1] x + [8]             
17.31/6.07	                 >  [1] x + [0]             
17.31/6.07	                 =  [c_3(x)]                
17.31/6.07	                                            
17.31/6.07	  [+^#(x, s(y))] =  [1] x + [1] y + [10]    
17.31/6.07	                 >  [1] x + [1] y + [8]     
17.31/6.07	                 =  [c_4(+^#(x, y))]        
17.31/6.07	                                            
17.31/6.07	
17.31/6.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Weak DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Weak Trs: { +(x, 0()) -> x }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	The weightgap principle applies (using the following nonconstant
17.31/6.07	growth matrix-interpretation)
17.31/6.07	
17.31/6.07	The following argument positions are usable:
17.31/6.07	  Uargs(s) = {1}, Uargs(+) = {1}, Uargs(c_2) = {1}, Uargs(+^#) = {1},
17.31/6.07	  Uargs(c_3) = {1}, Uargs(c_4) = {1}
17.31/6.07	
17.31/6.07	TcT has computed the following matrix interpretation satisfying
17.31/6.07	not(EDA) and not(IDA(1)).
17.31/6.07	
17.31/6.07	      [sum](x1) = [1] x1 + [4]
17.31/6.07	                              
17.31/6.07	            [0] = [5]         
17.31/6.07	                              
17.31/6.07	        [s](x1) = [1] x1 + [0]
17.31/6.07	                              
17.31/6.07	    [+](x1, x2) = [1] x1 + [4]
17.31/6.07	                              
17.31/6.07	    [sum^#](x1) = [1] x1 + [7]
17.31/6.07	                              
17.31/6.07	          [c_1] = [4]         
17.31/6.07	                              
17.31/6.07	      [c_2](x1) = [1] x1 + [0]
17.31/6.07	                              
17.31/6.07	  [+^#](x1, x2) = [1] x1 + [3]
17.31/6.07	                              
17.31/6.07	      [c_3](x1) = [1] x1 + [3]
17.31/6.07	                              
17.31/6.07	      [c_4](x1) = [1] x1 + [0]
17.31/6.07	
17.31/6.07	The order satisfies the following ordering constraints:
17.31/6.07	
17.31/6.07	      [sum(0())] =  [9]                     
17.31/6.07	                 >  [5]                     
17.31/6.07	                 =  [0()]                   
17.31/6.07	                                            
17.31/6.07	     [sum(s(x))] =  [1] x + [4]             
17.31/6.07	                 ?  [1] x + [8]             
17.31/6.07	                 =  [+(sum(x), s(x))]       
17.31/6.07	                                            
17.31/6.07	     [+(x, 0())] =  [1] x + [4]             
17.31/6.07	                 >  [1] x + [0]             
17.31/6.07	                 =  [x]                     
17.31/6.07	                                            
17.31/6.07	    [+(x, s(y))] =  [1] x + [4]             
17.31/6.07	                 >= [1] x + [4]             
17.31/6.07	                 =  [s(+(x, y))]            
17.31/6.07	                                            
17.31/6.07	    [sum^#(0())] =  [12]                    
17.31/6.07	                 >  [4]                     
17.31/6.07	                 =  [c_1()]                 
17.31/6.07	                                            
17.31/6.07	   [sum^#(s(x))] =  [1] x + [7]             
17.31/6.07	                 >= [1] x + [7]             
17.31/6.07	                 =  [c_2(+^#(sum(x), s(x)))]
17.31/6.07	                                            
17.31/6.07	   [+^#(x, 0())] =  [1] x + [3]             
17.31/6.07	                 >= [1] x + [3]             
17.31/6.07	                 =  [c_3(x)]                
17.31/6.07	                                            
17.31/6.07	  [+^#(x, s(y))] =  [1] x + [3]             
17.31/6.07	                 >= [1] x + [3]             
17.31/6.07	                 =  [c_4(+^#(x, y))]        
17.31/6.07	                                            
17.31/6.07	
17.31/6.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict Trs:
17.31/6.07	  { sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Weak DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Weak Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , +(x, 0()) -> x }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	The weightgap principle applies (using the following nonconstant
17.31/6.07	growth matrix-interpretation)
17.31/6.07	
17.31/6.07	The following argument positions are usable:
17.31/6.07	  Uargs(s) = {1}, Uargs(+) = {1}, Uargs(c_2) = {1}, Uargs(+^#) = {1},
17.31/6.07	  Uargs(c_3) = {1}, Uargs(c_4) = {1}
17.31/6.07	
17.31/6.07	TcT has computed the following matrix interpretation satisfying
17.31/6.07	not(EDA) and not(IDA(1)).
17.31/6.07	
17.31/6.07	      [sum](x1) = [1] x1 + [4]
17.31/6.07	                              
17.31/6.07	            [0] = [7]         
17.31/6.07	                              
17.31/6.07	        [s](x1) = [1] x1 + [4]
17.31/6.07	                              
17.31/6.07	    [+](x1, x2) = [1] x1 + [0]
17.31/6.07	                              
17.31/6.07	    [sum^#](x1) = [1] x1 + [7]
17.31/6.07	                              
17.31/6.07	          [c_1] = [5]         
17.31/6.07	                              
17.31/6.07	      [c_2](x1) = [1] x1 + [3]
17.31/6.07	                              
17.31/6.07	  [+^#](x1, x2) = [1] x1 + [3]
17.31/6.07	                              
17.31/6.07	      [c_3](x1) = [1] x1 + [3]
17.31/6.07	                              
17.31/6.07	      [c_4](x1) = [1] x1 + [0]
17.31/6.07	
17.31/6.07	The order satisfies the following ordering constraints:
17.31/6.07	
17.31/6.07	      [sum(0())] =  [11]                    
17.31/6.07	                 >  [7]                     
17.31/6.07	                 =  [0()]                   
17.31/6.07	                                            
17.31/6.07	     [sum(s(x))] =  [1] x + [8]             
17.31/6.07	                 >  [1] x + [4]             
17.31/6.07	                 =  [+(sum(x), s(x))]       
17.31/6.07	                                            
17.31/6.07	     [+(x, 0())] =  [1] x + [0]             
17.31/6.07	                 >= [1] x + [0]             
17.31/6.07	                 =  [x]                     
17.31/6.07	                                            
17.31/6.07	    [+(x, s(y))] =  [1] x + [0]             
17.31/6.07	                 ?  [1] x + [4]             
17.31/6.07	                 =  [s(+(x, y))]            
17.31/6.07	                                            
17.31/6.07	    [sum^#(0())] =  [14]                    
17.31/6.07	                 >  [5]                     
17.31/6.07	                 =  [c_1()]                 
17.31/6.07	                                            
17.31/6.07	   [sum^#(s(x))] =  [1] x + [11]            
17.31/6.07	                 >  [1] x + [10]            
17.31/6.07	                 =  [c_2(+^#(sum(x), s(x)))]
17.31/6.07	                                            
17.31/6.07	   [+^#(x, 0())] =  [1] x + [3]             
17.31/6.07	                 >= [1] x + [3]             
17.31/6.07	                 =  [c_3(x)]                
17.31/6.07	                                            
17.31/6.07	  [+^#(x, s(y))] =  [1] x + [3]             
17.31/6.07	                 >= [1] x + [3]             
17.31/6.07	                 =  [c_4(+^#(x, y))]        
17.31/6.07	                                            
17.31/6.07	
17.31/6.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(n^2)).
17.31/6.07	
17.31/6.07	Strict Trs: { +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Weak DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Weak Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(n^2))
17.31/6.07	
17.31/6.07	We use the processor 'polynomial interpretation' to orient
17.31/6.07	following rules strictly.
17.31/6.07	
17.31/6.07	Trs: { +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	
17.31/6.07	The induced complexity on above rules (modulo remaining rules) is
17.31/6.07	YES(?,O(n^2)) . These rules are moved into the corresponding weak
17.31/6.07	component(s).
17.31/6.07	
17.31/6.07	Sub-proof:
17.31/6.07	----------
17.31/6.07	  We consider the following typing:
17.31/6.07	  
17.31/6.07	    sum :: b -> b
17.31/6.07	    0 :: b
17.31/6.07	    s :: b -> b
17.31/6.07	    + :: (b,b) -> b
17.31/6.07	    sum^# :: b -> a
17.31/6.07	    c_1 :: a
17.31/6.07	    c_2 :: c -> a
17.31/6.07	    +^# :: (b,b) -> c
17.31/6.07	    c_3 :: b -> c
17.31/6.07	    c_4 :: c -> c
17.31/6.07	  
17.31/6.07	  The following argument positions are considered usable:
17.31/6.07	  
17.31/6.07	    Uargs(s) = {1}, Uargs(+) = {1}, Uargs(c_2) = {1}, Uargs(+^#) = {1},
17.31/6.07	    Uargs(c_3) = {1}, Uargs(c_4) = {1}
17.31/6.07	  
17.31/6.07	  TcT has computed the following constructor-restricted
17.31/6.07	  typedpolynomial interpretation.
17.31/6.07	  
17.31/6.07	      [sum](x1) = x1 + x1^2  
17.31/6.07	                             
17.31/6.07	          [0]() = 0          
17.31/6.07	                             
17.31/6.07	        [s](x1) = 1 + x1     
17.31/6.07	                             
17.31/6.07	    [+](x1, x2) = x1 + 2*x2  
17.31/6.07	                             
17.31/6.07	    [sum^#](x1) = x1 + 3*x1^2
17.31/6.07	                             
17.31/6.07	        [c_1]() = 0          
17.31/6.07	                             
17.31/6.07	      [c_2](x1) = x1         
17.31/6.07	                             
17.31/6.07	  [+^#](x1, x2) = x1         
17.31/6.07	                             
17.31/6.07	      [c_3](x1) = x1         
17.31/6.07	                             
17.31/6.07	      [c_4](x1) = x1         
17.31/6.07	                             
17.31/6.07	  
17.31/6.07	  This order satisfies the following ordering constraints.
17.31/6.07	  
17.31/6.07	      [sum(0())] =                   
17.31/6.07	                 >=                  
17.31/6.07	                 =  [0()]            
17.31/6.07	                                     
17.31/6.07	     [sum(s(x))] =  2 + 3*x + x^2    
17.31/6.07	                 >= 3*x + x^2 + 2    
17.31/6.07	                 =  [+(sum(x), s(x))]
17.31/6.07	                                     
17.31/6.07	     [+(x, 0())] =  x                
17.31/6.07	                 >= x                
17.31/6.07	                 =  [x]              
17.31/6.07	                                     
17.31/6.07	    [+(x, s(y))] =  x + 2 + 2*y      
17.31/6.07	                 >  1 + x + 2*y      
17.31/6.07	                 =  [s(+(x, y))]     
17.31/6.07	                                     
17.31/6.07	
17.31/6.07	We return to the main proof.
17.31/6.07	
17.31/6.07	We are left with following problem, upon which TcT provides the
17.31/6.07	certificate YES(O(1),O(1)).
17.31/6.07	
17.31/6.07	Weak DPs:
17.31/6.07	  { sum^#(0()) -> c_1()
17.31/6.07	  , sum^#(s(x)) -> c_2(+^#(sum(x), s(x)))
17.31/6.07	  , +^#(x, 0()) -> c_3(x)
17.31/6.07	  , +^#(x, s(y)) -> c_4(+^#(x, y)) }
17.31/6.07	Weak Trs:
17.31/6.07	  { sum(0()) -> 0()
17.31/6.07	  , sum(s(x)) -> +(sum(x), s(x))
17.31/6.07	  , +(x, 0()) -> x
17.31/6.07	  , +(x, s(y)) -> s(+(x, y)) }
17.31/6.07	Obligation:
17.31/6.07	  runtime complexity
17.31/6.07	Answer:
17.31/6.07	  YES(O(1),O(1))
17.31/6.07	
17.31/6.07	Empty rules are trivially bounded
17.31/6.07	
17.31/6.07	Hurray, we answered YES(O(1),O(n^2))
17.48/6.10	EOF