YES(O(1),O(n^1))
0.00/0.26	YES(O(1),O(n^1))
0.00/0.26	
0.00/0.26	We are left with following problem, upon which TcT provides the
0.00/0.26	certificate YES(O(1),O(n^1)).
0.00/0.26	
0.00/0.26	Strict Trs:
0.00/0.26	  { sum(0()) -> 0()
0.00/0.26	  , sum(s(x)) -> +(sqr(s(x)), sum(x))
0.00/0.26	  , sum(s(x)) -> +(*(s(x), s(x)), sum(x))
0.00/0.26	  , sqr(x) -> *(x, x) }
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(O(1),O(n^1))
0.00/0.26	
0.00/0.26	We add the following weak dependency pairs:
0.00/0.26	
0.00/0.26	Strict DPs:
0.00/0.26	  { sum^#(0()) -> c_1()
0.00/0.26	  , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	  , sum^#(s(x)) -> c_3(x, x, sum^#(x))
0.00/0.26	  , sqr^#(x) -> c_4(x, x) }
0.00/0.26	
0.00/0.26	and mark the set of starting terms.
0.00/0.26	
0.00/0.26	We are left with following problem, upon which TcT provides the
0.00/0.26	certificate YES(O(1),O(n^1)).
0.00/0.26	
0.00/0.26	Strict DPs:
0.00/0.26	  { sum^#(0()) -> c_1()
0.00/0.26	  , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	  , sum^#(s(x)) -> c_3(x, x, sum^#(x))
0.00/0.26	  , sqr^#(x) -> c_4(x, x) }
0.00/0.26	Strict Trs:
0.00/0.26	  { sum(0()) -> 0()
0.00/0.26	  , sum(s(x)) -> +(sqr(s(x)), sum(x))
0.00/0.26	  , sum(s(x)) -> +(*(s(x), s(x)), sum(x))
0.00/0.26	  , sqr(x) -> *(x, x) }
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(O(1),O(n^1))
0.00/0.26	
0.00/0.26	No rule is usable, rules are removed from the input problem.
0.00/0.26	
0.00/0.26	We are left with following problem, upon which TcT provides the
0.00/0.26	certificate YES(O(1),O(n^1)).
0.00/0.26	
0.00/0.26	Strict DPs:
0.00/0.26	  { sum^#(0()) -> c_1()
0.00/0.26	  , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	  , sum^#(s(x)) -> c_3(x, x, sum^#(x))
0.00/0.26	  , sqr^#(x) -> c_4(x, x) }
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(O(1),O(n^1))
0.00/0.26	
0.00/0.26	The weightgap principle applies (using the following constant
0.00/0.26	growth matrix-interpretation)
0.00/0.26	
0.00/0.26	The following argument positions are usable:
0.00/0.26	  Uargs(c_2) = {1, 2}, Uargs(c_3) = {3}
0.00/0.26	
0.00/0.26	TcT has computed the following constructor-restricted matrix
0.00/0.26	interpretation.
0.00/0.26	
0.00/0.26	                [0] = [0]                                 
0.00/0.26	                      [0]                                 
0.00/0.26	                                                          
0.00/0.26	            [s](x1) = [0]                                 
0.00/0.26	                      [0]                                 
0.00/0.26	                                                          
0.00/0.26	        [sum^#](x1) = [0]                                 
0.00/0.26	                      [0]                                 
0.00/0.26	                                                          
0.00/0.26	              [c_1] = [1]                                 
0.00/0.26	                      [0]                                 
0.00/0.26	                                                          
0.00/0.26	      [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0]           
0.00/0.26	                      [0 1]      [0 1]      [0]           
0.00/0.26	                                                          
0.00/0.26	        [sqr^#](x1) = [1]                                 
0.00/0.26	                      [1]                                 
0.00/0.26	                                                          
0.00/0.26	  [c_3](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [2]
0.00/0.26	                      [1 2]      [2 2]      [0 1]      [0]
0.00/0.26	                                                          
0.00/0.26	      [c_4](x1, x2) = [0]                                 
0.00/0.26	                      [1]                                 
0.00/0.26	
0.00/0.26	The order satisfies the following ordering constraints:
0.00/0.26	
0.00/0.26	   [sum^#(0())] = [0]                         
0.00/0.26	                  [0]                         
0.00/0.26	                ? [1]                         
0.00/0.26	                  [0]                         
0.00/0.26	                = [c_1()]                     
0.00/0.26	                                              
0.00/0.26	  [sum^#(s(x))] = [0]                         
0.00/0.26	                  [0]                         
0.00/0.26	                ? [1]                         
0.00/0.26	                  [1]                         
0.00/0.26	                = [c_2(sqr^#(s(x)), sum^#(x))]
0.00/0.26	                                              
0.00/0.26	  [sum^#(s(x))] = [0]                         
0.00/0.26	                  [0]                         
0.00/0.26	                ? [0 0] x + [2]               
0.00/0.26	                  [3 4]     [0]               
0.00/0.26	                = [c_3(x, x, sum^#(x))]       
0.00/0.26	                                              
0.00/0.26	     [sqr^#(x)] = [1]                         
0.00/0.26	                  [1]                         
0.00/0.26	                > [0]                         
0.00/0.26	                  [1]                         
0.00/0.26	                = [c_4(x, x)]                 
0.00/0.26	                                              
0.00/0.26	
0.00/0.26	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.26	
0.00/0.26	We are left with following problem, upon which TcT provides the
0.00/0.26	certificate YES(O(1),O(n^1)).
0.00/0.26	
0.00/0.26	Strict DPs:
0.00/0.26	  { sum^#(0()) -> c_1()
0.00/0.26	  , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	  , sum^#(s(x)) -> c_3(x, x, sum^#(x)) }
0.00/0.26	Weak DPs: { sqr^#(x) -> c_4(x, x) }
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(O(1),O(n^1))
0.00/0.26	
0.00/0.26	We use the processor 'matrix interpretation of dimension 1' to
0.00/0.26	orient following rules strictly.
0.00/0.26	
0.00/0.26	DPs:
0.00/0.26	  { 1: sum^#(0()) -> c_1()
0.00/0.26	  , 2: sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	  , 3: sum^#(s(x)) -> c_3(x, x, sum^#(x)) }
0.00/0.26	
0.00/0.26	Sub-proof:
0.00/0.26	----------
0.00/0.26	  The following argument positions are usable:
0.00/0.26	    Uargs(c_2) = {1, 2}, Uargs(c_3) = {3}
0.00/0.26	  
0.00/0.26	  TcT has computed the following constructor-based matrix
0.00/0.26	  interpretation satisfying not(EDA).
0.00/0.26	  
0.00/0.26	                  [0] = [3]                  
0.00/0.26	                                             
0.00/0.26	              [s](x1) = [1] x1 + [3]         
0.00/0.26	                                             
0.00/0.26	          [sum^#](x1) = [3] x1 + [0]         
0.00/0.26	                                             
0.00/0.26	                [c_1] = [0]                  
0.00/0.26	                                             
0.00/0.26	        [c_2](x1, x2) = [4] x1 + [1] x2 + [7]
0.00/0.26	                                             
0.00/0.26	          [sqr^#](x1) = [0]                  
0.00/0.26	                                             
0.00/0.26	    [c_3](x1, x2, x3) = [1] x3 + [7]         
0.00/0.26	                                             
0.00/0.26	        [c_4](x1, x2) = [0]                  
0.00/0.26	  
0.00/0.26	  The order satisfies the following ordering constraints:
0.00/0.26	  
0.00/0.26	     [sum^#(0())] =  [9]                         
0.00/0.26	                  >  [0]                         
0.00/0.26	                  =  [c_1()]                     
0.00/0.26	                                                 
0.00/0.26	    [sum^#(s(x))] =  [3] x + [9]                 
0.00/0.26	                  >  [3] x + [7]                 
0.00/0.26	                  =  [c_2(sqr^#(s(x)), sum^#(x))]
0.00/0.26	                                                 
0.00/0.26	    [sum^#(s(x))] =  [3] x + [9]                 
0.00/0.26	                  >  [3] x + [7]                 
0.00/0.26	                  =  [c_3(x, x, sum^#(x))]       
0.00/0.26	                                                 
0.00/0.26	       [sqr^#(x)] =  [0]                         
0.00/0.26	                  >= [0]                         
0.00/0.26	                  =  [c_4(x, x)]                 
0.00/0.26	                                                 
0.00/0.26	
0.00/0.26	The strictly oriented rules are moved into the weak component.
0.00/0.26	
0.00/0.26	We are left with following problem, upon which TcT provides the
0.00/0.26	certificate YES(O(1),O(1)).
0.00/0.26	
0.00/0.26	Weak DPs:
0.00/0.26	  { sum^#(0()) -> c_1()
0.00/0.26	  , sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	  , sum^#(s(x)) -> c_3(x, x, sum^#(x))
0.00/0.26	  , sqr^#(x) -> c_4(x, x) }
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(O(1),O(1))
0.00/0.26	
0.00/0.26	The following weak DPs constitute a sub-graph of the DG that is
0.00/0.26	closed under successors. The DPs are removed.
0.00/0.26	
0.00/0.26	{ sum^#(0()) -> c_1()
0.00/0.26	, sum^#(s(x)) -> c_2(sqr^#(s(x)), sum^#(x))
0.00/0.26	, sum^#(s(x)) -> c_3(x, x, sum^#(x))
0.00/0.26	, sqr^#(x) -> c_4(x, x) }
0.00/0.26	
0.00/0.26	We are left with following problem, upon which TcT provides the
0.00/0.26	certificate YES(O(1),O(1)).
0.00/0.26	
0.00/0.26	Rules: Empty
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(O(1),O(1))
0.00/0.26	
0.00/0.26	Empty rules are trivially bounded
0.00/0.26	
0.00/0.26	Hurray, we answered YES(O(1),O(n^1))
0.00/0.26	EOF