YES(?,O(n^1))

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

Strict Trs:
  { comp_f_g[1](walk_1(), walk_4(x11), x7) -> walk_4[1](x11, x7)
  , comp_f_g[1](comp_f_g(x7, walk_4(x9)), walk_4(x5), x3) ->
    comp_f_g[1](x7, walk_4(x9), walk_4[1](x5, x3))
  , walk_4[1](x7, x11) -> Cons(x7, x11)
  , rec[walk_0][1](Cons(x61, x77)) ->
    comp_f_g(rec[walk_0][1](x77), walk_4(x61))
  , rec[walk_0][1](Nil()) -> walk_1()
  , main(Cons(x122, x154)) ->
    comp_f_g[1](rec[walk_0][1](x154), walk_4(x122), Nil())
  , main(Nil()) -> 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.
{ walk_1_0() -> 2
, walk_1_1() -> 1
, walk_1_1() -> 4
, walk_4_0(2) -> 2
, walk_4_1(2) -> 3
, walk_4_2(2) -> 6
, comp_f_g[1]_0(2, 2, 2) -> 1
, comp_f_g[1]_1(2, 3, 1) -> 1
, comp_f_g[1]_1(4, 3, 5) -> 1
, comp_f_g[1]_2(4, 6, 1) -> 1
, walk_4[1]_0(2, 2) -> 1
, walk_4[1]_1(2, 1) -> 1
, walk_4[1]_1(2, 2) -> 1
, walk_4[1]_2(2, 1) -> 1
, walk_4[1]_2(2, 5) -> 1
, comp_f_g_0(2, 2) -> 2
, comp_f_g_1(4, 3) -> 1
, comp_f_g_1(4, 3) -> 4
, 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
, Cons_3(2, 5) -> 1
, Nil_0() -> 2
, Nil_1() -> 1
, Nil_1() -> 5
, rec[walk_0][1]_0(2) -> 1
, rec[walk_0][1]_1(2) -> 4
, main_0(2) -> 1 }

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