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)