YES(?,O(n^1))

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

Strict Trs:
  { rec[revApp_0][2](Nil(), Cons(x1, x2)) -> Cons(x1, x2)
  , rec[revApp_0][2](Cons(x14, x10), x6) ->
    rec[revApp_0][2](x10, Cons(x14, x6))
  , rec[dfsAcc_0][3](Leaf(x40), x56) -> Cons(x40, x56)
  , rec[dfsAcc_0][3](Node(x14, x10), x6) ->
    rec[dfsAcc_0][3](x10, rec[dfsAcc_0][3](x14, x6))
  , main(x1) ->
    rec[revApp_0][2](rec[dfsAcc_0][3](x1, Nil()), 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.
{ Nil_0() -> 2
, Nil_1() -> 1
, Nil_1() -> 4
, Cons_0(2, 2) -> 2
, Cons_1(2, 1) -> 1
, Cons_1(2, 2) -> 1
, Cons_1(2, 2) -> 2
, Cons_1(2, 2) -> 3
, Cons_1(2, 3) -> 1
, Cons_1(2, 3) -> 3
, Cons_1(2, 4) -> 1
, Cons_1(2, 4) -> 2
, Cons_1(2, 5) -> 1
, Cons_2(2, 1) -> 1
, Cons_2(2, 1) -> 5
, Cons_2(2, 2) -> 1
, Cons_2(2, 3) -> 1
, Cons_2(2, 5) -> 1
, Cons_2(2, 5) -> 5
, rec[revApp_0][2]_0(2, 2) -> 1
, rec[revApp_0][2]_1(2, 1) -> 1
, rec[revApp_0][2]_1(4, 3) -> 1
, rec[revApp_0][2]_2(2, 5) -> 1
, rec[revApp_0][2]_2(4, 5) -> 1
, Leaf_0(2) -> 2
, rec[dfsAcc_0][3]_0(2, 2) -> 1
, rec[dfsAcc_0][3]_1(2, 2) -> 2
, rec[dfsAcc_0][3]_1(2, 2) -> 3
, rec[dfsAcc_0][3]_1(2, 3) -> 1
, rec[dfsAcc_0][3]_1(2, 3) -> 3
, rec[dfsAcc_0][3]_1(2, 4) -> 2
, Node_0(2, 2) -> 2
, main_0(2) -> 1 }

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