YES(?,O(n^1))

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

Strict Trs:
  { rec[foldr_0][3](Nil()) -> fleft_0()
  , rec[foldr_0][3](Cons(x40, x14)) ->
    step_x_f(x40, rec[foldr_0][3](x14))
  , step_x_f[1](x11, fleft_0(), x7) -> rev_0[2](x7, x11)
  , step_x_f[1](x4, step_x_f(x3, x2), x1) ->
    step_x_f[1](x3, x2, rev_0[2](x1, x4))
  , rev_0[2](x6, x10) -> Cons(x10, x6)
  , main(Nil()) -> Nil()
  , main(Cons(x20, x25)) ->
    step_x_f[1](x20, rec[foldr_0][3](x25), Nil()) }
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.
{ Nil_0() -> 2
, Nil_1() -> 1
, rec[foldr_0][3]_0(2) -> 1
, rec[foldr_0][3]_1(2) -> 3
, fleft_0_0() -> 2
, fleft_0_1() -> 1
, fleft_0_1() -> 3
, Cons_0(2, 2) -> 2
, Cons_1(2, 2) -> 1
, Cons_2(2, 1) -> 1
, Cons_2(2, 2) -> 1
, Cons_3(2, 1) -> 1
, step_x_f_0(2, 2) -> 2
, step_x_f_1(2, 3) -> 1
, step_x_f_1(2, 3) -> 3
, step_x_f[1]_0(2, 2, 2) -> 1
, step_x_f[1]_1(2, 2, 1) -> 1
, step_x_f[1]_1(2, 3, 1) -> 1
, step_x_f[1]_2(2, 3, 1) -> 1
, rev_0[2]_0(2, 2) -> 1
, rev_0[2]_1(1, 2) -> 1
, rev_0[2]_1(2, 2) -> 1
, rev_0[2]_2(1, 2) -> 1
, main_0(2) -> 1 }

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