YES(?,O(n^1))

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

Strict Trs:
  { minus(n__0(), Y) -> 0()
  , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
  , 0() -> n__0()
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(X)
  , geq(X, n__0()) -> true()
  , geq(n__0(), n__s(Y)) -> false()
  , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
  , div(0(), n__s(Y)) -> 0()
  , div(s(X), n__s(Y)) ->
    if(geq(X, activate(Y)),
       n__s(div(minus(X, activate(Y)), n__s(activate(Y)))),
       n__0())
  , s(X) -> n__s(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

Arguments of following rules are not normal-forms:

{ div(0(), n__s(Y)) -> 0()
, div(s(X), n__s(Y)) ->
  if(geq(X, activate(Y)),
     n__s(div(minus(X, activate(Y)), n__s(activate(Y)))),
     n__0()) }

All above mentioned rules can be savely removed.

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

Strict Trs:
  { minus(n__0(), Y) -> 0()
  , minus(n__s(X), n__s(Y)) -> minus(activate(X), activate(Y))
  , 0() -> n__0()
  , activate(X) -> X
  , activate(n__0()) -> 0()
  , activate(n__s(X)) -> s(X)
  , geq(X, n__0()) -> true()
  , geq(n__0(), n__s(Y)) -> false()
  , geq(n__s(X), n__s(Y)) -> geq(activate(X), activate(Y))
  , s(X) -> n__s(X)
  , if(true(), X, Y) -> activate(X)
  , if(false(), X, Y) -> activate(Y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 4. The enriched problem is
compatible with the following automaton.
{ minus_0(2, 2) -> 1
, minus_1(3, 4) -> 1
, minus_2(5, 6) -> 1
, minus_3(7, 8) -> 1
, n__0_0() -> 1
, n__0_0() -> 2
, n__0_0() -> 3
, n__0_0() -> 4
, n__0_0() -> 5
, n__0_0() -> 6
, n__0_0() -> 7
, n__0_0() -> 8
, n__0_1() -> 1
, n__0_2() -> 1
, n__0_2() -> 3
, n__0_2() -> 4
, n__0_2() -> 5
, n__0_2() -> 6
, n__0_2() -> 7
, n__0_2() -> 8
, n__0_3() -> 1
, n__0_4() -> 1
, 0_0() -> 1
, 0_1() -> 1
, 0_1() -> 3
, 0_1() -> 4
, 0_1() -> 5
, 0_1() -> 6
, 0_1() -> 7
, 0_1() -> 8
, 0_2() -> 1
, 0_3() -> 1
, n__s_0(2) -> 1
, n__s_0(2) -> 2
, n__s_0(2) -> 3
, n__s_0(2) -> 4
, n__s_0(2) -> 5
, n__s_0(2) -> 6
, n__s_0(2) -> 7
, n__s_0(2) -> 8
, n__s_1(2) -> 1
, n__s_2(2) -> 1
, n__s_2(2) -> 3
, n__s_2(2) -> 4
, n__s_2(2) -> 5
, n__s_2(2) -> 6
, n__s_2(2) -> 7
, n__s_2(2) -> 8
, activate_0(2) -> 1
, activate_1(2) -> 1
, activate_1(2) -> 3
, activate_1(2) -> 4
, activate_2(2) -> 5
, activate_2(2) -> 6
, activate_3(2) -> 7
, activate_3(2) -> 8
, geq_0(2, 2) -> 1
, geq_1(4, 4) -> 1
, geq_2(6, 6) -> 1
, geq_3(8, 8) -> 1
, true_0() -> 1
, true_0() -> 2
, true_0() -> 3
, true_0() -> 4
, true_0() -> 5
, true_0() -> 6
, true_0() -> 7
, true_0() -> 8
, true_1() -> 1
, true_2() -> 1
, true_3() -> 1
, false_0() -> 1
, false_0() -> 2
, false_0() -> 3
, false_0() -> 4
, false_0() -> 5
, false_0() -> 6
, false_0() -> 7
, false_0() -> 8
, false_1() -> 1
, false_2() -> 1
, false_3() -> 1
, div_0(2, 2) -> 1
, s_0(2) -> 1
, s_1(2) -> 1
, s_1(2) -> 3
, s_1(2) -> 4
, s_1(2) -> 5
, s_1(2) -> 6
, s_1(2) -> 7
, s_1(2) -> 8
, if_0(2, 2, 2) -> 1
, 2 -> 1
, 2 -> 3
, 2 -> 4
, 2 -> 5
, 2 -> 6
, 2 -> 7
, 2 -> 8 }

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