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