YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { rec[foldr_0][3](Nil()) -> fleft_0() , rec[foldr_0][3](Cons(x40, x14)) -> step_x_f(x40, rec[foldr_0][3](x14)) , step_x_f[1](x11, fleft_0(), x7) -> rev_0[2](x7, x11) , step_x_f[1](x4, step_x_f(x3, x2), x1) -> step_x_f[1](x3, x2, rev_0[2](x1, x4)) , rev_0[2](x6, x10) -> Cons(x10, x6) , main(Nil()) -> Nil() , main(Cons(x20, x25)) -> step_x_f[1](x20, rec[foldr_0][3](x25), Nil()) } 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. { Nil_0() -> 2 , Nil_1() -> 1 , rec[foldr_0][3]_0(2) -> 1 , rec[foldr_0][3]_1(2) -> 3 , fleft_0_0() -> 2 , fleft_0_1() -> 1 , fleft_0_1() -> 3 , Cons_0(2, 2) -> 2 , Cons_1(2, 2) -> 1 , Cons_2(2, 1) -> 1 , Cons_2(2, 2) -> 1 , Cons_3(2, 1) -> 1 , step_x_f_0(2, 2) -> 2 , step_x_f_1(2, 3) -> 1 , step_x_f_1(2, 3) -> 3 , step_x_f[1]_0(2, 2, 2) -> 1 , step_x_f[1]_1(2, 2, 1) -> 1 , step_x_f[1]_1(2, 3, 1) -> 1 , step_x_f[1]_2(2, 3, 1) -> 1 , rev_0[2]_0(2, 2) -> 1 , rev_0[2]_1(1, 2) -> 1 , rev_0[2]_1(2, 2) -> 1 , rev_0[2]_2(1, 2) -> 1 , main_0(2) -> 1 } Hurray, we answered YES(?,O(n^1))