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