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))