YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { foldl(x, Cons(S(0()), xs)) -> foldl(S(x), xs)
  , foldl(a, Nil()) -> a
  , foldl(S(0()), Cons(x, xs)) -> foldl(S(x), xs)
  , foldr(a, Cons(x, xs)) -> op(x, foldr(a, xs))
  , foldr(a, Nil()) -> a
  , op(x, S(0())) -> S(x)
  , op(S(0()), y) -> S(y)
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , fold(a, xs) -> Cons(foldl(a, xs), Cons(foldr(a, xs), Nil())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.

Trs:
  { foldl(x, Cons(S(0()), xs)) -> foldl(S(x), xs)
  , foldl(a, Nil()) -> a
  , foldl(S(0()), Cons(x, xs)) -> foldl(S(x), xs)
  , foldr(a, Cons(x, xs)) -> op(x, foldr(a, xs))
  , foldr(a, Nil()) -> a
  , op(x, S(0())) -> S(x)
  , op(S(0()), y) -> S(y)
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , fold(a, xs) -> Cons(foldl(a, xs), Cons(foldr(a, xs), Nil())) }

The induced complexity on above rules (modulo remaining rules) is
YES(?,O(n^1)) . These rules are moved into the corresponding weak
component(s).

Sub-proof:
----------
  The input was oriented with the instance of 'Small Polynomial Path
  Order (PS,1-bounded)' as induced by the safe mapping
  
   safe(foldl) = {1}, safe(Cons) = {1, 2}, safe(S) = {1},
   safe(0) = {}, safe(foldr) = {}, safe(op) = {1, 2}, safe(Nil) = {},
   safe(notEmpty) = {}, safe(True) = {}, safe(False) = {},
   safe(fold) = {}
  
  and precedence
  
   foldl > op, foldr > op, notEmpty > foldl, notEmpty > foldr,
   notEmpty > op, fold > foldl, fold > foldr, fold > op,
   foldl ~ foldr, notEmpty ~ fold .
  
  Following symbols are considered recursive:
  
   {foldl, foldr}
  
  The recursion depth is 1.
  
  For your convenience, here are the satisfied ordering constraints:
  
    foldl(Cons(; S(; 0()),  xs); x) > foldl(xs; S(; x))                                    
                                                                                           
                    foldl(Nil(); a) > a                                                    
                                                                                           
    foldl(Cons(; x,  xs); S(; 0())) > foldl(xs; S(; x))                                    
                                                                                           
         foldr(a,  Cons(; x,  xs);) > op(; x,  foldr(a,  xs;))                             
                                                                                           
                  foldr(a,  Nil();) > a                                                    
                                                                                           
                 op(; x,  S(; 0())) > S(; x)                                               
                                                                                           
                 op(; S(; 0()),  y) > S(; y)                                               
                                                                                           
          notEmpty(Cons(; x,  xs);) > True()                                               
                                                                                           
                   notEmpty(Nil();) > False()                                              
                                                                                           
                      fold(a,  xs;) > Cons(; foldl(xs; a),  Cons(; foldr(a,  xs;),  Nil()))
                                                                                           

We return to the main proof.

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

Weak Trs:
  { foldl(x, Cons(S(0()), xs)) -> foldl(S(x), xs)
  , foldl(a, Nil()) -> a
  , foldl(S(0()), Cons(x, xs)) -> foldl(S(x), xs)
  , foldr(a, Cons(x, xs)) -> op(x, foldr(a, xs))
  , foldr(a, Nil()) -> a
  , op(x, S(0())) -> S(x)
  , op(S(0()), y) -> S(y)
  , notEmpty(Cons(x, xs)) -> True()
  , notEmpty(Nil()) -> False()
  , fold(a, xs) -> Cons(foldl(a, xs), Cons(foldr(a, xs), Nil())) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))