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 } Hurray, we answered YES(?,O(n^1))