We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { a__f(X) -> f(X) , a__f(0()) -> cons(0(), f(s(0()))) , a__f(s(0())) -> a__f(a__p(s(0()))) , a__p(X) -> p(X) , a__p(s(0())) -> 0() , mark(0()) -> 0() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(f(X)) -> a__f(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(p(X)) -> a__p(mark(X)) } Obligation: runtime complexity Answer: YES(?,O(n^1)) The input is overlay and right-linear. Switching to innermost rewriting. We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { a__f(X) -> f(X) , a__f(0()) -> cons(0(), f(s(0()))) , a__f(s(0())) -> a__f(a__p(s(0()))) , a__p(X) -> p(X) , a__p(s(0())) -> 0() , mark(0()) -> 0() , mark(cons(X1, X2)) -> cons(mark(X1), X2) , mark(f(X)) -> a__f(mark(X)) , mark(s(X)) -> s(mark(X)) , mark(p(X)) -> a__p(mark(X)) } 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. { a__f_0(2) -> 1 , a__f_0(3) -> 1 , a__f_0(4) -> 1 , a__f_0(5) -> 1 , a__f_0(8) -> 1 , a__f_1(13) -> 1 , a__f_1(14) -> 7 , a__f_1(14) -> 14 , a__f_2(17) -> 7 , a__f_2(17) -> 14 , 0_0() -> 2 , 0_1() -> 6 , 0_1() -> 7 , 0_1() -> 9 , 0_1() -> 12 , 0_1() -> 14 , 0_2() -> 7 , 0_2() -> 13 , 0_2() -> 14 , 0_3() -> 17 , cons_0(2, 2) -> 3 , cons_0(2, 3) -> 3 , cons_0(2, 4) -> 3 , cons_0(2, 5) -> 3 , cons_0(2, 8) -> 3 , cons_0(3, 2) -> 3 , cons_0(3, 3) -> 3 , cons_0(3, 4) -> 3 , cons_0(3, 5) -> 3 , cons_0(3, 8) -> 3 , cons_0(4, 2) -> 3 , cons_0(4, 3) -> 3 , cons_0(4, 4) -> 3 , cons_0(4, 5) -> 3 , cons_0(4, 8) -> 3 , cons_0(5, 2) -> 3 , cons_0(5, 3) -> 3 , cons_0(5, 4) -> 3 , cons_0(5, 5) -> 3 , cons_0(5, 8) -> 3 , cons_0(8, 2) -> 3 , cons_0(8, 3) -> 3 , cons_0(8, 4) -> 3 , cons_0(8, 5) -> 3 , cons_0(8, 8) -> 3 , cons_1(9, 10) -> 1 , cons_1(14, 2) -> 7 , cons_1(14, 2) -> 14 , cons_1(14, 3) -> 7 , cons_1(14, 3) -> 14 , cons_1(14, 4) -> 7 , cons_1(14, 4) -> 14 , cons_1(14, 5) -> 7 , cons_1(14, 5) -> 14 , cons_1(14, 8) -> 7 , cons_1(14, 8) -> 14 , cons_2(13, 15) -> 1 , cons_2(13, 15) -> 7 , cons_2(13, 15) -> 14 , cons_3(17, 18) -> 7 , cons_3(17, 18) -> 14 , f_0(2) -> 4 , f_0(3) -> 4 , f_0(4) -> 4 , f_0(5) -> 4 , f_0(8) -> 4 , f_1(2) -> 1 , f_1(3) -> 1 , f_1(4) -> 1 , f_1(5) -> 1 , f_1(8) -> 1 , f_1(11) -> 10 , f_2(13) -> 1 , f_2(14) -> 7 , f_2(14) -> 14 , f_2(16) -> 15 , f_3(17) -> 7 , f_3(17) -> 14 , f_3(19) -> 18 , s_0(2) -> 5 , s_0(3) -> 5 , s_0(4) -> 5 , s_0(5) -> 5 , s_0(8) -> 5 , s_1(12) -> 11 , s_1(14) -> 7 , s_1(14) -> 14 , s_2(13) -> 16 , s_3(17) -> 19 , a__p_0(2) -> 6 , a__p_0(3) -> 6 , a__p_0(4) -> 6 , a__p_0(5) -> 6 , a__p_0(8) -> 6 , a__p_1(11) -> 13 , a__p_1(14) -> 7 , a__p_1(14) -> 14 , a__p_2(16) -> 17 , mark_0(2) -> 7 , mark_0(3) -> 7 , mark_0(4) -> 7 , mark_0(5) -> 7 , mark_0(8) -> 7 , mark_1(2) -> 14 , mark_1(3) -> 14 , mark_1(4) -> 14 , mark_1(5) -> 14 , mark_1(8) -> 14 , p_0(2) -> 8 , p_0(3) -> 8 , p_0(4) -> 8 , p_0(5) -> 8 , p_0(8) -> 8 , p_1(2) -> 6 , p_1(3) -> 6 , p_1(4) -> 6 , p_1(5) -> 6 , p_1(8) -> 6 , p_2(11) -> 13 , p_2(14) -> 7 , p_2(14) -> 14 , p_3(16) -> 17 } Hurray, we answered YES(?,O(n^1))