YES(?,O(n^1))
0.00/0.26	YES(?,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(n^1)).
0.00/0.26	
0.00/0.26	Strict Trs:
0.00/0.26	  { +(0(), y) -> y
0.00/0.26	  , +(s(x), y) -> s(+(x, y))
0.00/0.26	  , -(x, 0()) -> x
0.00/0.26	  , -(0(), y) -> 0()
0.00/0.26	  , -(s(x), s(y)) -> -(x, y) }
0.00/0.26	Obligation:
0.00/0.26	  runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(?,O(n^1))
0.00/0.26	
0.00/0.26	The input is overlay and right-linear. Switching to innermost
0.00/0.26	rewriting.
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(n^1)).
0.00/0.26	
0.00/0.26	Strict Trs:
0.00/0.26	  { +(0(), y) -> y
0.00/0.26	  , +(s(x), y) -> s(+(x, y))
0.00/0.26	  , -(x, 0()) -> x
0.00/0.26	  , -(0(), y) -> 0()
0.00/0.26	  , -(s(x), s(y)) -> -(x, y) }
0.00/0.26	Obligation:
0.00/0.26	  innermost runtime complexity
0.00/0.26	Answer:
0.00/0.26	  YES(?,O(n^1))
0.00/0.26	
0.00/0.26	The input was oriented with the instance of 'Small Polynomial Path
0.00/0.26	Order (PS,1-bounded)' as induced by the safe mapping
0.00/0.26	
0.00/0.26	 safe(+) = {}, safe(0) = {}, safe(s) = {1}, safe(-) = {2}
0.00/0.26	
0.00/0.26	and precedence
0.00/0.26	
0.00/0.26	 empty .
0.00/0.26	
0.00/0.26	Following symbols are considered recursive:
0.00/0.26	
0.00/0.26	 {+, -}
0.00/0.26	
0.00/0.26	The recursion depth is 1.
0.00/0.26	
0.00/0.26	For your convenience, here are the satisfied ordering constraints:
0.00/0.26	
0.00/0.26	        +(0(),  y;) > y             
0.00/0.26	                                    
0.00/0.26	     +(s(; x),  y;) > s(; +(x,  y;))
0.00/0.26	                                    
0.00/0.26	          -(x; 0()) > x             
0.00/0.26	                                    
0.00/0.26	          -(0(); y) > 0()           
0.00/0.26	                                    
0.00/0.26	  -(s(; x); s(; y)) > -(x; y)       
0.00/0.26	                                    
0.00/0.26	
0.00/0.26	Hurray, we answered YES(?,O(n^1))
0.00/0.26	EOF