YES(?,O(n^1))

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

Strict Trs:
  { rec[iter_0][3](0()) -> id()
  , rec[iter_0][3](S(x14)) -> compS_f(rec[iter_0][3](x14))
  , compS_f[1](id(), x7) -> S(x7)
  , compS_f[1](compS_f(x5), x3) -> compS_f[1](x5, S(x3))
  , main(0()) -> 0()
  , main(S(x25)) -> compS_f[1](rec[iter_0][3](x25), 0()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 2. The enriched problem is
compatible with the following automaton.
{ 0_0() -> 1
, 0_1() -> 7
, rec[iter_0][3]_0(1) -> 2
, rec[iter_0][3]_0(3) -> 2
, rec[iter_0][3]_0(4) -> 2
, rec[iter_0][3]_0(5) -> 2
, rec[iter_0][3]_1(1) -> 8
, rec[iter_0][3]_1(3) -> 8
, rec[iter_0][3]_1(4) -> 8
, rec[iter_0][3]_1(5) -> 8
, id_0() -> 3
, id_1() -> 2
, id_1() -> 8
, S_0(1) -> 4
, S_0(3) -> 4
, S_0(4) -> 4
, S_0(5) -> 4
, S_1(1) -> 6
, S_1(3) -> 6
, S_1(4) -> 6
, S_1(5) -> 6
, S_1(6) -> 6
, S_2(7) -> 7
, compS_f_0(1) -> 5
, compS_f_0(3) -> 5
, compS_f_0(4) -> 5
, compS_f_0(5) -> 5
, compS_f_1(8) -> 2
, compS_f_1(8) -> 8
, compS_f[1]_0(1, 1) -> 6
, compS_f[1]_0(1, 3) -> 6
, compS_f[1]_0(1, 4) -> 6
, compS_f[1]_0(1, 5) -> 6
, compS_f[1]_0(3, 1) -> 6
, compS_f[1]_0(3, 3) -> 6
, compS_f[1]_0(3, 4) -> 6
, compS_f[1]_0(3, 5) -> 6
, compS_f[1]_0(4, 1) -> 6
, compS_f[1]_0(4, 3) -> 6
, compS_f[1]_0(4, 4) -> 6
, compS_f[1]_0(4, 5) -> 6
, compS_f[1]_0(5, 1) -> 6
, compS_f[1]_0(5, 3) -> 6
, compS_f[1]_0(5, 4) -> 6
, compS_f[1]_0(5, 5) -> 6
, compS_f[1]_1(1, 6) -> 6
, compS_f[1]_1(3, 6) -> 6
, compS_f[1]_1(4, 6) -> 6
, compS_f[1]_1(5, 6) -> 6
, compS_f[1]_1(8, 7) -> 7
, compS_f[1]_2(8, 7) -> 7
, main_0(1) -> 7
, main_0(3) -> 7
, main_0(4) -> 7
, main_0(5) -> 7 }

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