We are left with following problem, upon which TcT provides the certificate YES(?,POLY). Strict Trs: { cond_scanr_f_z_xs_1(Cons(0(), x11), 0()) -> Cons(0(), Cons(0(), x11)) , cond_scanr_f_z_xs_1(Cons(0(), x11), S(x2)) -> Cons(S(x2), Cons(0(), x11)) , cond_scanr_f_z_xs_1(Cons(0(), x11), M(x2)) -> Cons(0(), Cons(0(), x11)) , cond_scanr_f_z_xs_1(Cons(S(x2), x11), 0()) -> Cons(S(x2), Cons(S(x2), x11)) , cond_scanr_f_z_xs_1(Cons(S(x2), x11), S(x4)) -> Cons(plus#2(S(x4), S(x2)), Cons(S(x2), x11)) , cond_scanr_f_z_xs_1(Cons(S(x40), x23), M(0())) -> Cons(S(x40), Cons(S(x40), x23)) , cond_scanr_f_z_xs_1(Cons(S(x8), x23), M(S(x4))) -> Cons(minus#2(x8, x4), Cons(S(x8), x23)) , minus#2(0(), x16) -> 0() , minus#2(S(x20), 0()) -> S(x20) , minus#2(S(x4), S(x2)) -> minus#2(x4, x2) , plus#2(0(), S(x2)) -> S(x2) , plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) , scanr#3(Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2), x4) , scanr#3(Nil()) -> Cons(0(), Nil()) , foldl#3(x6, Cons(x4, x2)) -> foldl#3(max#2(x6, x4), x2) , foldl#3(x2, Nil()) -> x2 , max#2(0(), x8) -> x8 , max#2(S(x12), 0()) -> S(x12) , max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) , main(x1) -> foldl#3(0(), scanr#3(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(cond_scanr_f_z_xs_1) = {1}, safe(Cons) = {1, 2}, safe(0) = {}, safe(S) = {1}, safe(M) = {1}, safe(minus#2) = {1}, safe(plus#2) = {2}, safe(scanr#3) = {}, safe(Nil) = {}, safe(foldl#3) = {1}, safe(max#2) = {1}, safe(main) = {} and precedence cond_scanr_f_z_xs_1 > minus#2, cond_scanr_f_z_xs_1 > plus#2, scanr#3 > cond_scanr_f_z_xs_1, foldl#3 > max#2, main > scanr#3, main > foldl#3 . Following symbols are considered recursive: {minus#2, plus#2, scanr#3, foldl#3, max#2, main} The recursion depth is 3. For your convenience, here are the satisfied ordering constraints: cond_scanr_f_z_xs_1(0(); Cons(; 0(), x11)) > Cons(; 0(), Cons(; 0(), x11)) cond_scanr_f_z_xs_1(S(; x2); Cons(; 0(), x11)) > Cons(; S(; x2), Cons(; 0(), x11)) cond_scanr_f_z_xs_1(M(; x2); Cons(; 0(), x11)) > Cons(; 0(), Cons(; 0(), x11)) cond_scanr_f_z_xs_1(0(); Cons(; S(; x2), x11)) > Cons(; S(; x2), Cons(; S(; x2), x11)) cond_scanr_f_z_xs_1(S(; x4); Cons(; S(; x2), x11)) > Cons(; plus#2(S(; x4); S(; x2)), Cons(; S(; x2), x11)) cond_scanr_f_z_xs_1(M(; 0()); Cons(; S(; x40), x23)) > Cons(; S(; x40), Cons(; S(; x40), x23)) cond_scanr_f_z_xs_1(M(; S(; x4)); Cons(; S(; x8), x23)) > Cons(; minus#2(x4; x8), Cons(; S(; x8), x23)) minus#2(x16; 0()) > 0() minus#2(0(); S(; x20)) > S(; x20) minus#2(S(; x2); S(; x4)) > minus#2(x2; x4) plus#2(0(); S(; x2)) > S(; x2) plus#2(S(; x4); S(; x2)) > S(; plus#2(x4; S(; x2))) scanr#3(Cons(; x4, x2);) > cond_scanr_f_z_xs_1(x4; scanr#3(x2;)) scanr#3(Nil();) > Cons(; 0(), Nil()) foldl#3(Cons(; x4, x2); x6) > foldl#3(x2; max#2(x4; x6)) foldl#3(Nil(); x2) > x2 max#2(x8; 0()) > x8 max#2(0(); S(; x12)) > S(; x12) max#2(S(; x2); S(; x4)) > S(; max#2(x2; x4)) main(x1;) > foldl#3(scanr#3(x1;); 0()) Hurray, we answered YES(?,POLY)