YES(?,O(n^1))

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

Strict Trs:
  { append(@l1, @l2) -> append#1(@l1, @l2)
  , append#1(::(@x, @xs), @l2) -> ::(@x, append(@xs, @l2))
  , append#1(nil(), @l2) -> @l2
  , appendAll(@l) -> appendAll#1(@l)
  , appendAll#1(::(@l1, @ls)) -> append(@l1, appendAll(@ls))
  , appendAll#1(nil()) -> nil()
  , appendAll2(@l) -> appendAll2#1(@l)
  , appendAll2#1(::(@l1, @ls)) ->
    append(appendAll(@l1), appendAll2(@ls))
  , appendAll2#1(nil()) -> nil()
  , appendAll3(@l) -> appendAll3#1(@l)
  , appendAll3#1(::(@l1, @ls)) ->
    append(appendAll2(@l1), appendAll3(@ls))
  , appendAll3#1(nil()) -> nil() }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 4. The enriched problem is
compatible with the following automaton.
{ append_0(2, 2) -> 1
, append_1(2, 2) -> 3
, append_1(2, 4) -> 1
, append_1(2, 4) -> 4
, append_1(4, 5) -> 1
, append_1(4, 5) -> 5
, append_1(4, 5) -> 7
, append_1(5, 6) -> 1
, append_1(5, 6) -> 6
, append_1(5, 6) -> 8
, append_2(4, 5) -> 7
, append_3(7, 6) -> 8
, append#1_0(2, 2) -> 1
, append#1_1(2, 2) -> 1
, append#1_2(2, 2) -> 3
, append#1_2(2, 4) -> 1
, append#1_2(2, 4) -> 4
, append#1_2(4, 5) -> 1
, append#1_2(4, 5) -> 5
, append#1_2(4, 5) -> 7
, append#1_2(5, 6) -> 1
, append#1_2(5, 6) -> 6
, append#1_2(5, 6) -> 8
, append#1_3(4, 5) -> 7
, append#1_4(7, 6) -> 8
, ::_0(2, 2) -> 1
, ::_0(2, 2) -> 2
, ::_0(2, 2) -> 3
, ::_1(2, 1) -> 1
, ::_1(2, 3) -> 1
, ::_1(2, 3) -> 3
, ::_1(2, 4) -> 1
, ::_1(2, 4) -> 4
, ::_2(2, 7) -> 1
, ::_2(2, 7) -> 5
, ::_2(2, 7) -> 7
, ::_3(2, 8) -> 1
, ::_3(2, 8) -> 6
, ::_3(2, 8) -> 8
, nil_0() -> 1
, nil_0() -> 2
, nil_0() -> 3
, nil_1() -> 1
, nil_1() -> 4
, nil_1() -> 5
, nil_1() -> 6
, nil_1() -> 7
, nil_1() -> 8
, appendAll_0(2) -> 1
, appendAll_1(2) -> 1
, appendAll_1(2) -> 4
, appendAll#1_0(2) -> 1
, appendAll#1_1(2) -> 1
, appendAll#1_2(2) -> 1
, appendAll#1_2(2) -> 4
, appendAll2_0(2) -> 1
, appendAll2_1(2) -> 1
, appendAll2_1(2) -> 5
, appendAll2_1(2) -> 7
, appendAll2#1_0(2) -> 1
, appendAll2#1_1(2) -> 1
, appendAll2#1_2(2) -> 1
, appendAll2#1_2(2) -> 5
, appendAll2#1_2(2) -> 7
, appendAll3_0(2) -> 1
, appendAll3_1(2) -> 1
, appendAll3_1(2) -> 6
, appendAll3_1(2) -> 8
, appendAll3#1_0(2) -> 1
, appendAll3#1_1(2) -> 1
, appendAll3#1_2(2) -> 1
, appendAll3#1_2(2) -> 6
, appendAll3#1_2(2) -> 8
, 2 -> 1
, 2 -> 3
, 4 -> 1
, 5 -> 1
, 5 -> 7
, 6 -> 1
, 6 -> 8 }

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