YES(?,O(n^1))
11.50/3.17	YES(?,O(n^1))
11.50/3.17	
11.50/3.17	We are left with following problem, upon which TcT provides the
11.50/3.17	certificate YES(?,O(n^1)).
11.50/3.17	
11.50/3.17	Strict Trs:
11.50/3.17	  { f(X) -> n__f(X)
11.50/3.17	  , f(0()) -> cons(0(), n__f(n__s(n__0())))
11.50/3.17	  , f(s(0())) -> f(p(s(0())))
11.50/3.17	  , 0() -> n__0()
11.50/3.17	  , s(X) -> n__s(X)
11.50/3.17	  , p(s(0())) -> 0()
11.50/3.17	  , activate(X) -> X
11.50/3.17	  , activate(n__f(X)) -> f(activate(X))
11.50/3.17	  , activate(n__s(X)) -> s(activate(X))
11.50/3.17	  , activate(n__0()) -> 0() }
11.50/3.17	Obligation:
11.50/3.17	  runtime complexity
11.50/3.17	Answer:
11.50/3.17	  YES(?,O(n^1))
11.50/3.17	
11.50/3.17	The problem is match-bounded by 4. The enriched problem is
11.50/3.17	compatible with the following automaton.
11.50/3.17	{ f_0(2) -> 1
11.50/3.17	, f_1(3) -> 1
11.50/3.17	, f_1(3) -> 3
11.50/3.17	, f_2(8) -> 1
11.50/3.17	, f_2(8) -> 3
11.50/3.17	, 0_0() -> 1
11.50/3.17	, 0_1() -> 1
11.50/3.17	, 0_1() -> 3
11.50/3.17	, 0_2() -> 4
11.50/3.17	, 0_3() -> 8
11.50/3.17	, cons_0(2, 2) -> 1
11.50/3.17	, cons_0(2, 2) -> 2
11.50/3.17	, cons_0(2, 2) -> 3
11.50/3.17	, cons_2(4, 5) -> 1
11.50/3.17	, cons_2(4, 5) -> 3
11.50/3.17	, cons_3(8, 10) -> 1
11.50/3.17	, cons_3(8, 10) -> 3
11.50/3.17	, n__f_0(2) -> 1
11.50/3.17	, n__f_0(2) -> 2
11.50/3.17	, n__f_0(2) -> 3
11.50/3.17	, n__f_1(2) -> 1
11.50/3.17	, n__f_2(3) -> 1
11.50/3.17	, n__f_2(3) -> 3
11.50/3.17	, n__f_2(6) -> 5
11.50/3.17	, n__f_3(8) -> 1
11.50/3.17	, n__f_3(8) -> 3
11.50/3.17	, n__f_3(9) -> 10
11.50/3.17	, n__s_0(2) -> 1
11.50/3.17	, n__s_0(2) -> 2
11.50/3.17	, n__s_0(2) -> 3
11.50/3.17	, n__s_1(2) -> 1
11.50/3.17	, n__s_2(3) -> 1
11.50/3.17	, n__s_2(3) -> 3
11.50/3.17	, n__s_2(7) -> 6
11.50/3.17	, n__s_3(4) -> 9
11.50/3.17	, n__0_0() -> 1
11.50/3.17	, n__0_0() -> 2
11.50/3.17	, n__0_0() -> 3
11.50/3.17	, n__0_1() -> 1
11.50/3.17	, n__0_2() -> 1
11.50/3.17	, n__0_2() -> 3
11.50/3.17	, n__0_2() -> 7
11.50/3.17	, n__0_3() -> 4
11.50/3.17	, n__0_4() -> 8
11.50/3.17	, s_0(2) -> 1
11.50/3.17	, s_1(3) -> 1
11.50/3.17	, s_1(3) -> 3
11.50/3.17	, s_2(4) -> 9
11.50/3.17	, p_0(2) -> 1
11.50/3.17	, p_2(9) -> 8
11.50/3.17	, activate_0(2) -> 1
11.50/3.17	, activate_1(2) -> 3 }
11.50/3.17	
11.50/3.17	Hurray, we answered YES(?,O(n^1))
11.50/3.18	EOF