YES(?,O(n^1))

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

Strict Trs:
  { cons_x[1](x2, x1) -> Cons(x2, x1)
  , comp_f_g[1](cons_x(x3), cons_x(x2), x1) ->
    cons_x[1](x3, cons_x[1](x2, x1))
  , comp_f_g[1](cons_x(x4), comp_f_g(x3, x2), x1) ->
    cons_x[1](x4, comp_f_g[1](x3, x2, x1))
  , comp_f_g[1](comp_f_g(x4, x3), cons_x(x2), x1) ->
    comp_f_g[1](x4, x3, cons_x[1](x2, x1))
  , comp_f_g[1](comp_f_g(x5, x4), comp_f_g(x3, x2), x1) ->
    comp_f_g[1](x5, x4, comp_f_g[1](x3, x2, x1))
  , rec[walk_0][1](Leaf(x1)) -> cons_x(x1)
  , rec[walk_0][1](Node(x2, x1)) ->
    comp_f_g(rec[walk_0][1](x2), rec[walk_0][1](x1))
  , main(Leaf(x2)) -> cons_x[1](x2, Nil())
  , main(Node(x4, x2)) ->
    comp_f_g[1](rec[walk_0][1](x4), rec[walk_0][1](x2), 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.
{ cons_x[1]_0(2, 2) -> 1
, cons_x[1]_1(2, 2) -> 3
, cons_x[1]_1(2, 3) -> 1
, cons_x[1]_1(2, 3) -> 3
, cons_x[1]_2(2, 3) -> 6
, cons_x[1]_2(2, 6) -> 1
, cons_x[1]_2(2, 6) -> 6
, Cons_0(2, 2) -> 2
, Cons_1(2, 2) -> 1
, Cons_2(2, 2) -> 3
, Cons_2(2, 3) -> 1
, Cons_2(2, 3) -> 3
, Cons_3(2, 3) -> 6
, Cons_3(2, 6) -> 1
, Cons_3(2, 6) -> 6
, cons_x_0(2) -> 2
, cons_x_1(2) -> 1
, cons_x_1(2) -> 4
, cons_x_1(2) -> 5
, comp_f_g_0(2, 2) -> 2
, comp_f_g_1(4, 5) -> 1
, comp_f_g_1(5, 5) -> 4
, comp_f_g_1(5, 5) -> 5
, comp_f_g[1]_0(2, 2, 2) -> 1
, comp_f_g[1]_1(2, 2, 2) -> 3
, comp_f_g[1]_1(2, 2, 3) -> 1
, comp_f_g[1]_1(2, 2, 3) -> 3
, comp_f_g[1]_1(5, 5, 3) -> 1
, comp_f_g[1]_2(5, 5, 3) -> 6
, comp_f_g[1]_2(5, 5, 6) -> 1
, comp_f_g[1]_2(5, 5, 6) -> 6
, Leaf_0(2) -> 2
, rec[walk_0][1]_0(2) -> 1
, rec[walk_0][1]_1(2) -> 4
, rec[walk_0][1]_1(2) -> 5
, Node_0(2, 2) -> 2
, main_0(2) -> 1
, Nil_0() -> 2
, Nil_1() -> 3 }

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