YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { f(X) -> n__f(X)
  , f(0()) -> cons(0(), n__f(n__s(n__0())))
  , f(s(0())) -> f(p(s(0())))
  , 0() -> n__0()
  , s(X) -> n__s(X)
  , p(s(X)) -> X
  , activate(X) -> X
  , activate(n__f(X)) -> f(activate(X))
  , activate(n__s(X)) -> s(activate(X))
  , activate(n__0()) -> 0() }
Obligation:
  runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 4. The enriched problem is
compatible with the following automaton.
{ f_0(2) -> 1
, f_1(3) -> 1
, f_1(3) -> 3
, f_2(8) -> 1
, f_2(8) -> 3
, 0_0() -> 1
, 0_1() -> 1
, 0_1() -> 3
, 0_2() -> 4
, 0_2() -> 8
, 0_3() -> 10
, cons_0(2, 2) -> 1
, cons_0(2, 2) -> 2
, cons_0(2, 2) -> 3
, cons_2(4, 5) -> 1
, cons_2(8, 5) -> 3
, cons_3(10, 11) -> 1
, cons_3(10, 11) -> 3
, n__f_0(2) -> 1
, n__f_0(2) -> 2
, n__f_0(2) -> 3
, n__f_1(2) -> 1
, n__f_2(3) -> 1
, n__f_2(3) -> 3
, n__f_2(6) -> 5
, n__f_3(8) -> 1
, n__f_3(8) -> 3
, n__f_3(9) -> 11
, n__s_0(2) -> 1
, n__s_0(2) -> 2
, n__s_0(2) -> 3
, n__s_1(2) -> 1
, n__s_2(3) -> 1
, n__s_2(3) -> 3
, n__s_2(7) -> 6
, n__s_3(4) -> 9
, n__0_0() -> 1
, n__0_0() -> 2
, n__0_0() -> 3
, n__0_1() -> 1
, n__0_2() -> 1
, n__0_2() -> 3
, n__0_2() -> 7
, n__0_3() -> 4
, n__0_3() -> 8
, n__0_4() -> 10
, s_0(2) -> 1
, s_1(3) -> 1
, s_1(3) -> 3
, s_2(4) -> 9
, p_0(2) -> 1
, p_2(9) -> 8
, activate_0(2) -> 1
, activate_1(2) -> 3
, 2 -> 1
, 2 -> 3
, 4 -> 8 }

Hurray, we answered YES(?,O(n^1))