YES(?,O(n^1))
34.12/19.92	YES(?,O(n^1))
34.12/19.92	
34.12/19.92	We are left with following problem, upon which TcT provides the
34.12/19.92	certificate YES(?,O(n^1)).
34.12/19.92	
34.12/19.92	Strict Trs:
34.12/19.92	  { f(X) -> n__f(X)
34.12/19.92	  , f(0()) -> cons(0(), n__f(s(0())))
34.12/19.92	  , f(s(0())) -> f(p(s(0())))
34.12/19.92	  , p(s(0())) -> 0()
34.12/19.92	  , activate(X) -> X
34.12/19.92	  , activate(n__f(X)) -> f(X) }
34.12/19.92	Obligation:
34.12/19.92	  derivational complexity
34.12/19.92	Answer:
34.12/19.92	  YES(?,O(n^1))
34.12/19.92	
34.12/19.92	The problem is match-bounded by 2. The enriched problem is
34.12/19.92	compatible with the following automaton.
34.12/19.92	{ f_0(1) -> 1
34.12/19.92	, f_1(1) -> 1
34.12/19.92	, f_1(6) -> 1
34.12/19.92	, 0_0() -> 1
34.12/19.92	, 0_1() -> 1
34.12/19.92	, 0_1() -> 2
34.12/19.92	, 0_1() -> 5
34.12/19.92	, 0_2() -> 6
34.12/19.92	, cons_0(1, 1) -> 1
34.12/19.92	, cons_1(2, 3) -> 1
34.12/19.92	, cons_2(6, 7) -> 1
34.12/19.92	, n__f_0(1) -> 1
34.12/19.92	, n__f_1(1) -> 1
34.12/19.92	, n__f_1(4) -> 3
34.12/19.92	, n__f_2(1) -> 1
34.12/19.92	, n__f_2(6) -> 1
34.12/19.92	, n__f_2(8) -> 7
34.12/19.92	, s_0(1) -> 1
34.12/19.92	, s_1(5) -> 4
34.12/19.92	, s_2(6) -> 8
34.12/19.92	, p_0(1) -> 1
34.12/19.92	, p_1(4) -> 6
34.12/19.92	, activate_0(1) -> 1 }
34.12/19.92	
34.12/19.92	Hurray, we answered YES(?,O(n^1))
34.12/19.93	EOF