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