We are left with following problem, upon which TcT provides the certificate YES(?,POLY). Strict Trs: { sum#1(Nil()) -> 0() , sum#1(Cons(x2, x1)) -> plus#2(x2, sum#1(x1)) , plus#2(0(), x8) -> x8 , plus#2(S(x4), x2) -> S(plus#2(x4, x2)) , map#2(Nil()) -> Nil() , map#2(Cons(x2, x5)) -> Cons(mult#2(x2, x2), map#2(x5)) , mult#2(0(), x2) -> 0() , mult#2(S(x4), x2) -> plus#2(x2, mult#2(x4, x2)) , unfoldr#2(0()) -> Nil() , unfoldr#2(S(x2)) -> Cons(x2, unfoldr#2(x2)) , main(0()) -> 0() , main(S(x1)) -> sum#1(map#2(Cons(S(x1), unfoldr#2(S(x1))))) } Obligation: innermost runtime complexity Answer: YES(?,POLY) The input was oriented with the instance of 'Polynomial Path Order (PS)' as induced by the safe mapping safe(sum#1) = {}, safe(Nil) = {}, safe(0) = {}, safe(Cons) = {1, 2}, safe(plus#2) = {2}, safe(map#2) = {}, safe(mult#2) = {}, safe(unfoldr#2) = {}, safe(S) = {1}, safe(main) = {} and precedence sum#1 > plus#2, map#2 > mult#2, mult#2 > plus#2, main > sum#1, main > map#2, main > unfoldr#2 . Following symbols are considered recursive: {sum#1, plus#2, map#2, mult#2, unfoldr#2, main} The recursion depth is 4. For your convenience, here are the satisfied ordering constraints: sum#1(Nil();) > 0() sum#1(Cons(; x2, x1);) > plus#2(x2; sum#1(x1;)) plus#2(0(); x8) > x8 plus#2(S(; x4); x2) > S(; plus#2(x4; x2)) map#2(Nil();) > Nil() map#2(Cons(; x2, x5);) > Cons(; mult#2(x2, x2;), map#2(x5;)) mult#2(0(), x2;) > 0() mult#2(S(; x4), x2;) > plus#2(x2; mult#2(x4, x2;)) unfoldr#2(0();) > Nil() unfoldr#2(S(; x2);) > Cons(; x2, unfoldr#2(x2;)) main(0();) > 0() main(S(; x1);) > sum#1(map#2(Cons(; S(; x1), unfoldr#2(S(; x1);)););) Hurray, we answered YES(?,POLY)