YES(?,O(n^1))

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

Strict Trs:
  { foldr_f[3](NilF()) -> 0()
  , foldr_f[3](ConsF(plus_x(x2), x1)) ->
    comp_f_g[1](plus_x(x2), rec[foldr_0][3](x1))
  , rec[foldr_0][3](NilF()) -> id()
  , rec[foldr_0][3](ConsF(plus_x(x2), x1)) ->
    comp_f_g(plus_x(x2), rec[foldr_0][3](x1))
  , comp_f_g[1](plus_x(x7), id()) -> plus_x[1](x7, 0())
  , comp_f_g[1](plus_x(x3), comp_f_g(plus_x(x2), x1)) ->
    plus_x[1](x3, comp_f_g[1](plus_x(x2), x1))
  , plus_x[1](0(), x9) -> x9
  , plus_x[1](S(x10), x4) -> S(plus_x[1](x10, x4))
  , rec[mapF_0][2](Nil()) -> NilF()
  , rec[mapF_0][2](Cons(x20, x14)) ->
    ConsF(plus_x(x20), rec[mapF_0][2](x14))
  , main(x7) -> foldr_f[3](rec[mapF_0][2](x7)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 3. The enriched problem is
compatible with the following automaton.
{ NilF_0() -> 1
, NilF_0() -> 2
, NilF_1() -> 1
, NilF_1() -> 7
, foldr_f[3]_0(2) -> 1
, foldr_f[3]_1(7) -> 1
, 0_0() -> 1
, 0_0() -> 2
, 0_1() -> 1
, 0_2() -> 1
, 0_2() -> 5
, 0_2() -> 8
, 0_3() -> 1
, 0_3() -> 5
, 0_3() -> 8
, plus_x_0(2) -> 1
, plus_x_0(2) -> 2
, plus_x_1(2) -> 3
, plus_x_2(2) -> 6
, plus_x_3(2) -> 9
, ConsF_0(2, 2) -> 1
, ConsF_0(2, 2) -> 2
, ConsF_1(3, 7) -> 1
, ConsF_1(3, 7) -> 7
, rec[foldr_0][3]_0(2) -> 1
, rec[foldr_0][3]_1(2) -> 4
, rec[foldr_0][3]_2(7) -> 4
, comp_f_g[1]_0(2, 2) -> 1
, comp_f_g[1]_1(3, 2) -> 1
, comp_f_g[1]_1(3, 4) -> 1
, comp_f_g[1]_2(6, 4) -> 1
, comp_f_g[1]_2(6, 4) -> 5
, comp_f_g[1]_2(6, 4) -> 8
, comp_f_g[1]_3(9, 4) -> 1
, comp_f_g[1]_3(9, 4) -> 5
, comp_f_g[1]_3(9, 4) -> 8
, id_0() -> 1
, id_0() -> 2
, id_1() -> 1
, id_1() -> 4
, id_2() -> 4
, comp_f_g_0(2, 2) -> 1
, comp_f_g_0(2, 2) -> 2
, comp_f_g_1(3, 4) -> 1
, comp_f_g_1(3, 4) -> 4
, comp_f_g_2(6, 4) -> 4
, plus_x[1]_0(2, 2) -> 1
, plus_x[1]_1(2, 1) -> 1
, plus_x[1]_1(2, 2) -> 1
, plus_x[1]_1(2, 5) -> 1
, plus_x[1]_1(2, 8) -> 1
, plus_x[1]_2(2, 5) -> 1
, plus_x[1]_2(2, 5) -> 5
, plus_x[1]_2(2, 5) -> 8
, plus_x[1]_3(2, 8) -> 1
, plus_x[1]_3(2, 8) -> 5
, plus_x[1]_3(2, 8) -> 8
, Nil_0() -> 1
, Nil_0() -> 2
, rec[mapF_0][2]_0(2) -> 1
, rec[mapF_0][2]_1(2) -> 7
, Cons_0(2, 2) -> 1
, Cons_0(2, 2) -> 2
, S_0(2) -> 1
, S_0(2) -> 2
, S_1(1) -> 1
, S_1(1) -> 5
, S_1(1) -> 8
, main_0(2) -> 1
, 2 -> 1
, 5 -> 1
, 5 -> 8
, 8 -> 1
, 8 -> 5 }

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