YES(?,O(n^1))
0.00/0.82	YES(?,O(n^1))
0.00/0.82	
0.00/0.82	We are left with following problem, upon which TcT provides the
0.00/0.82	certificate YES(?,O(n^1)).
0.00/0.82	
0.00/0.82	Strict Trs:
0.00/0.82	  { f(0()) -> s(0())
0.00/0.82	  , f(s(0())) -> s(0())
0.00/0.82	  , f(s(s(x))) -> f(f(s(x))) }
0.00/0.82	Obligation:
0.00/0.82	  runtime complexity
0.00/0.82	Answer:
0.00/0.82	  YES(?,O(n^1))
0.00/0.82	
0.00/0.82	The input is overlay and right-linear. Switching to innermost
0.00/0.82	rewriting.
0.00/0.82	
0.00/0.82	We are left with following problem, upon which TcT provides the
0.00/0.82	certificate YES(?,O(n^1)).
0.00/0.82	
0.00/0.82	Strict Trs:
0.00/0.82	  { f(0()) -> s(0())
0.00/0.82	  , f(s(0())) -> s(0())
0.00/0.82	  , f(s(s(x))) -> f(f(s(x))) }
0.00/0.82	Obligation:
0.00/0.82	  innermost runtime complexity
0.00/0.82	Answer:
0.00/0.82	  YES(?,O(n^1))
0.00/0.82	
0.00/0.82	The problem is match-bounded by 2. The enriched problem is
0.00/0.82	compatible with the following automaton.
0.00/0.82	{ f_0(2) -> 1
0.00/0.82	, f_0(3) -> 1
0.00/0.82	, f_1(5) -> 1
0.00/0.82	, f_1(5) -> 5
0.00/0.82	, f_1(6) -> 5
0.00/0.82	, 0_0() -> 2
0.00/0.82	, 0_1() -> 4
0.00/0.82	, 0_2() -> 7
0.00/0.82	, s_0(2) -> 3
0.00/0.82	, s_0(3) -> 3
0.00/0.82	, s_1(2) -> 6
0.00/0.82	, s_1(3) -> 6
0.00/0.82	, s_1(4) -> 1
0.00/0.82	, s_1(4) -> 5
0.00/0.82	, s_2(7) -> 1
0.00/0.82	, s_2(7) -> 5 }
0.00/0.82	
0.00/0.82	Hurray, we answered YES(?,O(n^1))
0.00/0.83	EOF