YES(?,POLY)

We are left with following problem, upon which TcT provides the
certificate YES(?,POLY).

Strict Trs:
  { rec[plus_0][2](0(), x50) -> x50
  , rec[plus_0][2](S(x10), x6) -> S(rec[plus_0][2](x10, x6))
  , rec[sum_0][1](Nil()) -> 0()
  , rec[sum_0][1](Cons(x5, x3)) ->
    rec[plus_0][2](x5, rec[sum_0][1](x3))
  , rec[map_0][2](Nil()) -> Nil()
  , rec[map_0][2](Cons(x6, x13)) ->
    Cons(rec[mult_0][2](x6, x6), rec[map_0][2](x13))
  , rec[mult_0][2](0(), x34) -> 0()
  , rec[mult_0][2](S(x10), x6) ->
    rec[plus_0][2](x6, rec[mult_0][2](x10, x6))
  , rec[unfoldr_0][2](0()) -> Nil()
  , rec[unfoldr_0][2](S(x6)) -> Cons(x6, rec[unfoldr_0][2](x6))
  , main(0()) -> 0()
  , main(S(x1)) ->
    rec[sum_0][1](rec[map_0][2](Cons(S(x1),
                                     rec[unfoldr_0][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(0) = {}, safe(rec[plus_0][2]) = {2}, safe(S) = {1},
 safe(Nil) = {}, safe(rec[sum_0][1]) = {}, safe(Cons) = {1, 2},
 safe(rec[map_0][2]) = {}, safe(rec[mult_0][2]) = {},
 safe(rec[unfoldr_0][2]) = {}, safe(main) = {}

and precedence

 rec[sum_0][1] > rec[plus_0][2], rec[sum_0][1] > rec[mult_0][2],
 rec[map_0][2] > rec[plus_0][2], rec[map_0][2] > rec[mult_0][2],
 rec[mult_0][2] > rec[plus_0][2],
 rec[unfoldr_0][2] > rec[plus_0][2],
 rec[unfoldr_0][2] > rec[mult_0][2], main > rec[plus_0][2],
 main > rec[sum_0][1], main > rec[map_0][2], main > rec[mult_0][2],
 main > rec[unfoldr_0][2], rec[sum_0][1] ~ rec[map_0][2],
 rec[sum_0][1] ~ rec[unfoldr_0][2],
 rec[map_0][2] ~ rec[unfoldr_0][2] .

Following symbols are considered recursive:

 {rec[plus_0][2], rec[sum_0][1], rec[map_0][2], rec[mult_0][2],
  rec[unfoldr_0][2], main}

The recursion depth is 4.

For your convenience, here are the satisfied ordering constraints:

          rec[plus_0][2](0(); x50) > x50                                                                
                                                                                                        
      rec[plus_0][2](S(; x10); x6) > S(; rec[plus_0][2](x10; x6))                                       
                                                                                                        
             rec[sum_0][1](Nil();) > 0()                                                                
                                                                                                        
   rec[sum_0][1](Cons(; x5,  x3);) > rec[plus_0][2](x5; rec[sum_0][1](x3;))                             
                                                                                                        
             rec[map_0][2](Nil();) > Nil()                                                              
                                                                                                        
  rec[map_0][2](Cons(; x6,  x13);) > Cons(; rec[mult_0][2](x6,  x6;),  rec[map_0][2](x13;))             
                                                                                                        
        rec[mult_0][2](0(),  x34;) > 0()                                                                
                                                                                                        
    rec[mult_0][2](S(; x10),  x6;) > rec[plus_0][2](x6; rec[mult_0][2](x10,  x6;))                      
                                                                                                        
           rec[unfoldr_0][2](0();) > Nil()                                                              
                                                                                                        
       rec[unfoldr_0][2](S(; x6);) > Cons(; x6,  rec[unfoldr_0][2](x6;))                                
                                                                                                        
                        main(0();) > 0()                                                                
                                                                                                        
                    main(S(; x1);) > rec[sum_0][1](rec[map_0][2](Cons(; S(; x1),                        
                                                                        rec[unfoldr_0][2](S(; x1);)););)
                                                                                                        

Hurray, we answered YES(?,POLY)