YES(?,O(n^1))
0.00/0.15	YES(?,O(n^1))
0.00/0.15	
0.00/0.15	We are left with following problem, upon which TcT provides the
0.00/0.15	certificate YES(?,O(n^1)).
0.00/0.15	
0.00/0.15	Strict Trs:
0.00/0.15	  { sum(0()) -> 0()
0.00/0.15	  , sum(s(x)) -> +(sum(x), s(x))
0.00/0.15	  , sum1(0()) -> 0()
0.00/0.15	  , sum1(s(x)) -> s(+(sum1(x), +(x, x))) }
0.00/0.15	Obligation:
0.00/0.15	  innermost runtime complexity
0.00/0.15	Answer:
0.00/0.15	  YES(?,O(n^1))
0.00/0.15	
0.00/0.15	The input was oriented with the instance of 'Small Polynomial Path
0.00/0.15	Order (PS)' as induced by the safe mapping
0.00/0.15	
0.00/0.15	 safe(sum) = {}, safe(0) = {}, safe(s) = {1}, safe(+) = {1, 2},
0.00/0.15	 safe(sum1) = {}
0.00/0.15	
0.00/0.15	and precedence
0.00/0.15	
0.00/0.15	 sum ~ sum1 .
0.00/0.15	
0.00/0.15	Following symbols are considered recursive:
0.00/0.15	
0.00/0.15	 {sum, sum1}
0.00/0.15	
0.00/0.15	The recursion depth is 1.
0.00/0.15	
0.00/0.15	For your convenience, here are the satisfied ordering constraints:
0.00/0.15	
0.00/0.15	      sum(0();) > 0()                            
0.00/0.15	                                                 
0.00/0.15	   sum(s(; x);) > +(; sum(x;),  s(; x))          
0.00/0.15	                                                 
0.00/0.15	     sum1(0();) > 0()                            
0.00/0.15	                                                 
0.00/0.15	  sum1(s(; x);) > s(; +(; sum1(x;),  +(; x,  x)))
0.00/0.15	                                                 
0.00/0.15	
0.00/0.15	Hurray, we answered YES(?,O(n^1))
0.00/0.15	EOF