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

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

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