YES(?,O(n^1))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).
Strict Trs:
{ rec[take_l_0][2](0()) -> Nil()
, rec[take_l_0][2](S(x6)) -> Cons(rec[take_l_0][2](x6))
, main(x3) -> rec[take_l_0][2](x3) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^1))
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(0) = {}, safe(rec[take_l_0][2]) = {}, safe(Nil) = {},
safe(S) = {1}, safe(Cons) = {1}, safe(main) = {}
and precedence
main > rec[take_l_0][2] .
Following symbols are considered recursive:
{rec[take_l_0][2]}
The recursion depth is 1.
For your convenience, here are the satisfied ordering constraints:
rec[take_l_0][2](0();) > Nil()
rec[take_l_0][2](S(; x6);) > Cons(; rec[take_l_0][2](x6;))
main(x3;) > rec[take_l_0][2](x3;)
Hurray, we answered YES(?,O(n^1))