YES(O(1),O(n^1))
0.00/0.87	YES(O(1),O(n^1))
0.00/0.87	
0.00/0.87	We are left with following problem, upon which TcT provides the
0.00/0.87	certificate YES(O(1),O(n^1)).
0.00/0.87	
0.00/0.87	Strict Trs:
0.00/0.87	  { foldl(x, Cons(S(0()), xs)) -> foldl(S(x), xs)
0.00/0.87	  , foldl(a, Nil()) -> a
0.00/0.87	  , foldl(S(0()), Cons(x, xs)) -> foldl(S(x), xs)
0.00/0.87	  , foldr(a, Cons(x, xs)) -> op(x, foldr(a, xs))
0.00/0.87	  , foldr(a, Nil()) -> a
0.00/0.87	  , op(x, S(0())) -> S(x)
0.00/0.87	  , op(S(0()), y) -> S(y)
0.00/0.87	  , notEmpty(Cons(x, xs)) -> True()
0.00/0.87	  , notEmpty(Nil()) -> False()
0.00/0.87	  , fold(a, xs) -> Cons(foldl(a, xs), Cons(foldr(a, xs), Nil())) }
0.00/0.87	Obligation:
0.00/0.87	  innermost runtime complexity
0.00/0.87	Answer:
0.00/0.87	  YES(O(1),O(n^1))
0.00/0.87	
0.00/0.87	We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
0.00/0.87	to orient following rules strictly.
0.00/0.87	
0.00/0.87	Trs:
0.00/0.87	  { foldl(x, Cons(S(0()), xs)) -> foldl(S(x), xs)
0.00/0.87	  , foldl(a, Nil()) -> a
0.00/0.87	  , foldl(S(0()), Cons(x, xs)) -> foldl(S(x), xs)
0.00/0.87	  , foldr(a, Cons(x, xs)) -> op(x, foldr(a, xs))
0.00/0.87	  , foldr(a, Nil()) -> a
0.00/0.87	  , op(x, S(0())) -> S(x)
0.00/0.87	  , op(S(0()), y) -> S(y)
0.00/0.87	  , notEmpty(Cons(x, xs)) -> True()
0.00/0.87	  , notEmpty(Nil()) -> False()
0.00/0.87	  , fold(a, xs) -> Cons(foldl(a, xs), Cons(foldr(a, xs), Nil())) }
0.00/0.87	
0.00/0.87	The induced complexity on above rules (modulo remaining rules) is
0.00/0.87	YES(?,O(n^1)) . These rules are moved into the corresponding weak
0.00/0.87	component(s).
0.00/0.87	
0.00/0.87	Sub-proof:
0.00/0.87	----------
0.00/0.87	  The input was oriented with the instance of 'Small Polynomial Path
0.00/0.87	  Order (PS,1-bounded)' as induced by the safe mapping
0.00/0.87	  
0.00/0.87	   safe(foldl) = {1}, safe(Cons) = {1, 2}, safe(S) = {1},
0.00/0.87	   safe(0) = {}, safe(foldr) = {}, safe(op) = {1, 2}, safe(Nil) = {},
0.00/0.87	   safe(notEmpty) = {}, safe(True) = {}, safe(False) = {},
0.00/0.87	   safe(fold) = {}
0.00/0.87	  
0.00/0.87	  and precedence
0.00/0.87	  
0.00/0.87	   foldl > op, foldr > op, notEmpty > foldl, notEmpty > foldr,
0.00/0.87	   notEmpty > op, fold > foldl, fold > foldr, fold > op,
0.00/0.87	   foldl ~ foldr, notEmpty ~ fold .
0.00/0.87	  
0.00/0.87	  Following symbols are considered recursive:
0.00/0.87	  
0.00/0.87	   {foldl, foldr}
0.00/0.87	  
0.00/0.87	  The recursion depth is 1.
0.00/0.87	  
0.00/0.87	  For your convenience, here are the satisfied ordering constraints:
0.00/0.87	  
0.00/0.87	    foldl(Cons(; S(; 0()),  xs); x) > foldl(xs; S(; x))                                    
0.00/0.87	                                                                                           
0.00/0.87	                    foldl(Nil(); a) > a                                                    
0.00/0.87	                                                                                           
0.00/0.87	    foldl(Cons(; x,  xs); S(; 0())) > foldl(xs; S(; x))                                    
0.00/0.87	                                                                                           
0.00/0.87	         foldr(a,  Cons(; x,  xs);) > op(; x,  foldr(a,  xs;))                             
0.00/0.87	                                                                                           
0.00/0.87	                  foldr(a,  Nil();) > a                                                    
0.00/0.87	                                                                                           
0.00/0.87	                 op(; x,  S(; 0())) > S(; x)                                               
0.00/0.87	                                                                                           
0.00/0.87	                 op(; S(; 0()),  y) > S(; y)                                               
0.00/0.87	                                                                                           
0.00/0.87	          notEmpty(Cons(; x,  xs);) > True()                                               
0.00/0.87	                                                                                           
0.00/0.87	                   notEmpty(Nil();) > False()                                              
0.00/0.87	                                                                                           
0.00/0.87	                      fold(a,  xs;) > Cons(; foldl(xs; a),  Cons(; foldr(a,  xs;),  Nil()))
0.00/0.87	                                                                                           
0.00/0.87	
0.00/0.87	We return to the main proof.
0.00/0.87	
0.00/0.87	We are left with following problem, upon which TcT provides the
0.00/0.87	certificate YES(O(1),O(1)).
0.00/0.87	
0.00/0.87	Weak Trs:
0.00/0.87	  { foldl(x, Cons(S(0()), xs)) -> foldl(S(x), xs)
0.00/0.87	  , foldl(a, Nil()) -> a
0.00/0.87	  , foldl(S(0()), Cons(x, xs)) -> foldl(S(x), xs)
0.00/0.87	  , foldr(a, Cons(x, xs)) -> op(x, foldr(a, xs))
0.00/0.87	  , foldr(a, Nil()) -> a
0.00/0.87	  , op(x, S(0())) -> S(x)
0.00/0.87	  , op(S(0()), y) -> S(y)
0.00/0.87	  , notEmpty(Cons(x, xs)) -> True()
0.00/0.87	  , notEmpty(Nil()) -> False()
0.00/0.87	  , fold(a, xs) -> Cons(foldl(a, xs), Cons(foldr(a, xs), Nil())) }
0.00/0.87	Obligation:
0.00/0.87	  innermost runtime complexity
0.00/0.87	Answer:
0.00/0.87	  YES(O(1),O(1))
0.00/0.87	
0.00/0.87	Empty rules are trivially bounded
0.00/0.87	
0.00/0.87	Hurray, we answered YES(O(1),O(n^1))
0.00/0.88	EOF