YES(?,POLY) We are left with following problem, upon which TcT provides the certificate YES(?,POLY). Strict Trs: { rec[foldl_0][3](x6, Nil()) -> x6 , rec[foldl_0][3](x14, Cons(x10, x6)) -> rec[foldl_0][3](rec[max_0][2](x14, x10), x6) , rec[max_0][2](0(), x26) -> x26 , rec[max_0][2](S(x34), 0()) -> S(x34) , rec[max_0][2](S(x10), S(x6)) -> S(rec[max_0][2](x10, x6)) , scanr_cond_1(Cons(0(), x23), 0()) -> Cons(0(), Cons(0(), x23)) , scanr_cond_1(Cons(0(), x23), S(x70)) -> Cons(S(x70), Cons(0(), x23)) , scanr_cond_1(Cons(0(), x23), M(x34)) -> Cons(0(), Cons(0(), x23)) , scanr_cond_1(Cons(S(x34), x23), 0()) -> Cons(S(x34), Cons(S(x34), x23)) , scanr_cond_1(Cons(S(x6), x23), S(x10)) -> Cons(rec[plus_0][2](S(x10), S(x6)), Cons(S(x6), x23)) , scanr_cond_1(Cons(S(x2), x1), M(0())) -> Cons(S(x2), Cons(S(x2), x1)) , scanr_cond_1(Cons(S(x20), x47), M(S(x12))) -> Cons(rec[minus_0][2](x20, x12), Cons(S(x20), x47)) , rec[minus_0][2](0(), x58) -> 0() , rec[minus_0][2](S(x66), 0()) -> S(x66) , rec[minus_0][2](S(x10), S(x6)) -> rec[minus_0][2](x10, x6) , rec[plus_0][2](0(), S(x6)) -> S(x6) , rec[plus_0][2](S(x10), S(x6)) -> S(rec[plus_0][2](x10, S(x6))) , rec[scanr_0][3](Nil()) -> Cons(0(), Nil()) , rec[scanr_0][3](Cons(x10, x6)) -> scanr_cond_1(rec[scanr_0][3](x6), x10) , main(x1) -> rec[foldl_0][3](0(), rec[scanr_0][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(Nil) = {}, safe(rec[foldl_0][3]) = {1}, safe(Cons) = {1, 2}, safe(rec[max_0][2]) = {1}, safe(0) = {}, safe(S) = {1}, safe(scanr_cond_1) = {1}, safe(M) = {1}, safe(rec[minus_0][2]) = {1}, safe(rec[plus_0][2]) = {2}, safe(rec[scanr_0][3]) = {}, safe(main) = {} and precedence rec[foldl_0][3] > rec[max_0][2], rec[foldl_0][3] > scanr_cond_1, rec[foldl_0][3] > rec[minus_0][2], rec[foldl_0][3] > rec[plus_0][2], rec[max_0][2] > scanr_cond_1, rec[max_0][2] > rec[minus_0][2], rec[max_0][2] > rec[plus_0][2], scanr_cond_1 > rec[minus_0][2], scanr_cond_1 > rec[plus_0][2], rec[scanr_0][3] > rec[max_0][2], rec[scanr_0][3] > scanr_cond_1, rec[scanr_0][3] > rec[minus_0][2], rec[scanr_0][3] > rec[plus_0][2], main > rec[foldl_0][3], main > rec[max_0][2], main > scanr_cond_1, main > rec[minus_0][2], main > rec[plus_0][2], main > rec[scanr_0][3], rec[foldl_0][3] ~ rec[scanr_0][3], rec[minus_0][2] ~ rec[plus_0][2] . Following symbols are considered recursive: {rec[foldl_0][3], rec[max_0][2], scanr_cond_1, rec[minus_0][2], rec[plus_0][2], rec[scanr_0][3], main} The recursion depth is 5. For your convenience, here are the satisfied ordering constraints: rec[foldl_0][3](Nil(); x6) > x6 rec[foldl_0][3](Cons(; x10, x6); x14) > rec[foldl_0][3](x6; rec[max_0][2](x10; x14)) rec[max_0][2](x26; 0()) > x26 rec[max_0][2](0(); S(; x34)) > S(; x34) rec[max_0][2](S(; x6); S(; x10)) > S(; rec[max_0][2](x6; x10)) scanr_cond_1(0(); Cons(; 0(), x23)) > Cons(; 0(), Cons(; 0(), x23)) scanr_cond_1(S(; x70); Cons(; 0(), x23)) > Cons(; S(; x70), Cons(; 0(), x23)) scanr_cond_1(M(; x34); Cons(; 0(), x23)) > Cons(; 0(), Cons(; 0(), x23)) scanr_cond_1(0(); Cons(; S(; x34), x23)) > Cons(; S(; x34), Cons(; S(; x34), x23)) scanr_cond_1(S(; x10); Cons(; S(; x6), x23)) > Cons(; rec[plus_0][2](S(; x10); S(; x6)), Cons(; S(; x6), x23)) scanr_cond_1(M(; 0()); Cons(; S(; x2), x1)) > Cons(; S(; x2), Cons(; S(; x2), x1)) scanr_cond_1(M(; S(; x12)); Cons(; S(; x20), x47)) > Cons(; rec[minus_0][2](x12; x20), Cons(; S(; x20), x47)) rec[minus_0][2](x58; 0()) > 0() rec[minus_0][2](0(); S(; x66)) > S(; x66) rec[minus_0][2](S(; x6); S(; x10)) > rec[minus_0][2](x6; x10) rec[plus_0][2](0(); S(; x6)) > S(; x6) rec[plus_0][2](S(; x10); S(; x6)) > S(; rec[plus_0][2](x10; S(; x6))) rec[scanr_0][3](Nil();) > Cons(; 0(), Nil()) rec[scanr_0][3](Cons(; x10, x6);) > scanr_cond_1(x10; rec[scanr_0][3](x6;)) main(x1;) > rec[foldl_0][3](rec[scanr_0][3](x1;); 0()) Hurray, we answered YES(?,POLY)