YES(O(1),O(n^3))
79.07/31.65	YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^3)).
79.07/31.65	
79.07/31.65	Strict Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y
79.07/31.65	  , goal(xs, ys) -> mul0(xs, ys) }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	We add the following dependency tuples:
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	  , mul0^#(Nil(), y) -> c_2()
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	  , add0^#(Nil(), y) -> c_4()
79.07/31.65	  , goal^#(xs, ys) -> c_5(mul0^#(xs, ys)) }
79.07/31.65	
79.07/31.65	and mark the set of starting terms.
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^3)).
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	  , mul0^#(Nil(), y) -> c_2()
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	  , add0^#(Nil(), y) -> c_4()
79.07/31.65	  , goal^#(xs, ys) -> c_5(mul0^#(xs, ys)) }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y
79.07/31.65	  , goal(xs, ys) -> mul0(xs, ys) }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	We estimate the number of application of {2,4} by applications of
79.07/31.65	Pre({2,4}) = {1,3,5}. Here rules are labeled as follows:
79.07/31.65	
79.07/31.65	  DPs:
79.07/31.65	    { 1: mul0^#(Cons(x, xs), y) ->
79.07/31.65	         c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	    , 2: mul0^#(Nil(), y) -> c_2()
79.07/31.65	    , 3: add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	    , 4: add0^#(Nil(), y) -> c_4()
79.07/31.65	    , 5: goal^#(xs, ys) -> c_5(mul0^#(xs, ys)) }
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^3)).
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	  , goal^#(xs, ys) -> c_5(mul0^#(xs, ys)) }
79.07/31.65	Weak DPs:
79.07/31.65	  { mul0^#(Nil(), y) -> c_2()
79.07/31.65	  , add0^#(Nil(), y) -> c_4() }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y
79.07/31.65	  , goal(xs, ys) -> mul0(xs, ys) }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	The following weak DPs constitute a sub-graph of the DG that is
79.07/31.65	closed under successors. The DPs are removed.
79.07/31.65	
79.07/31.65	{ mul0^#(Nil(), y) -> c_2()
79.07/31.65	, add0^#(Nil(), y) -> c_4() }
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^3)).
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	  , goal^#(xs, ys) -> c_5(mul0^#(xs, ys)) }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y
79.07/31.65	  , goal(xs, ys) -> mul0(xs, ys) }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	Consider the dependency graph
79.07/31.65	
79.07/31.65	  1: mul0^#(Cons(x, xs), y) ->
79.07/31.65	     c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	     -->_1 add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) :2
79.07/31.65	     -->_2 mul0^#(Cons(x, xs), y) ->
79.07/31.65	           c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) :1
79.07/31.65	  
79.07/31.65	  2: add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	     -->_1 add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) :2
79.07/31.65	  
79.07/31.65	  3: goal^#(xs, ys) -> c_5(mul0^#(xs, ys))
79.07/31.65	     -->_1 mul0^#(Cons(x, xs), y) ->
79.07/31.65	           c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) :1
79.07/31.65	  
79.07/31.65	
79.07/31.65	Following roots of the dependency graph are removed, as the
79.07/31.65	considered set of starting terms is closed under reduction with
79.07/31.65	respect to these rules (modulo compound contexts).
79.07/31.65	
79.07/31.65	  { goal^#(xs, ys) -> c_5(mul0^#(xs, ys)) }
79.07/31.65	
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^3)).
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y
79.07/31.65	  , goal(xs, ys) -> mul0(xs, ys) }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	We replace rewrite rules by usable rules:
79.07/31.65	
79.07/31.65	  Weak Usable Rules:
79.07/31.65	    { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	    , mul0(Nil(), y) -> Nil()
79.07/31.65	    , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	    , add0(Nil(), y) -> y }
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^3)).
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y))
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^3))
79.07/31.65	
79.07/31.65	We decompose the input problem according to the dependency graph
79.07/31.65	into the upper component
79.07/31.65	
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) }
79.07/31.65	
79.07/31.65	and lower component
79.07/31.65	
79.07/31.65	  { add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) }
79.07/31.65	
79.07/31.65	Further, following extension rules are added to the lower
79.07/31.65	component.
79.07/31.65	
79.07/31.65	{ mul0^#(Cons(x, xs), y) -> mul0^#(xs, y)
79.07/31.65	, mul0^#(Cons(x, xs), y) -> add0^#(mul0(xs, y), y) }
79.07/31.65	
79.07/31.65	TcT solves the upper component with certificate YES(O(1),O(n^1)).
79.07/31.65	
79.07/31.65	Sub-proof:
79.07/31.65	----------
79.07/31.65	  We are left with following problem, upon which TcT provides the
79.07/31.65	  certificate YES(O(1),O(n^1)).
79.07/31.65	  
79.07/31.65	  Strict DPs:
79.07/31.65	    { mul0^#(Cons(x, xs), y) ->
79.07/31.65	      c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) }
79.07/31.65	  Weak Trs:
79.07/31.65	    { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	    , mul0(Nil(), y) -> Nil()
79.07/31.65	    , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	    , add0(Nil(), y) -> y }
79.07/31.65	  Obligation:
79.07/31.65	    innermost runtime complexity
79.07/31.65	  Answer:
79.07/31.65	    YES(O(1),O(n^1))
79.07/31.65	  
79.07/31.65	  We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
79.07/31.65	  to orient following rules strictly.
79.07/31.65	  
79.07/31.65	  DPs:
79.07/31.65	    { 1: mul0^#(Cons(x, xs), y) ->
79.07/31.65	         c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) }
79.07/31.65	  
79.07/31.65	  Sub-proof:
79.07/31.65	  ----------
79.07/31.65	    The input was oriented with the instance of 'Small Polynomial Path
79.07/31.65	    Order (PS,1-bounded)' as induced by the safe mapping
79.07/31.65	    
79.07/31.65	     safe(mul0) = {}, safe(Cons) = {1, 2}, safe(add0) = {},
79.07/31.65	     safe(S) = {}, safe(Nil) = {}, safe(mul0^#) = {2}, safe(c_1) = {},
79.07/31.65	     safe(add0^#) = {}
79.07/31.65	    
79.07/31.65	    and precedence
79.07/31.65	    
79.07/31.65	     mul0^# > add0, mul0 ~ add0 .
79.07/31.65	    
79.07/31.65	    Following symbols are considered recursive:
79.07/31.65	    
79.07/31.65	     {mul0^#}
79.07/31.65	    
79.07/31.65	    The recursion depth is 1.
79.07/31.65	    
79.07/31.65	    Further, following argument filtering is employed:
79.07/31.65	    
79.07/31.65	     pi(mul0) = 2, pi(Cons) = [2], pi(add0) = 2, pi(S) = [],
79.07/31.65	     pi(Nil) = [], pi(mul0^#) = [1], pi(c_1) = [1, 2], pi(add0^#) = []
79.07/31.65	    
79.07/31.65	    Usable defined function symbols are a subset of:
79.07/31.65	    
79.07/31.65	     {mul0^#, add0^#}
79.07/31.65	    
79.07/31.65	    For your convenience, here are the satisfied ordering constraints:
79.07/31.65	    
79.07/31.65	      pi(mul0^#(Cons(x, xs), y)) = mul0^#(Cons(; xs);)                           
79.07/31.65	                                 > c_1(add0^#(),  mul0^#(xs;);)                  
79.07/31.65	                                 = pi(c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)))
79.07/31.65	                                                                                 
79.07/31.65	  
79.07/31.65	  The strictly oriented rules are moved into the weak component.
79.07/31.65	  
79.07/31.65	  We are left with following problem, upon which TcT provides the
79.07/31.65	  certificate YES(O(1),O(1)).
79.07/31.65	  
79.07/31.65	  Weak DPs:
79.07/31.65	    { mul0^#(Cons(x, xs), y) ->
79.07/31.65	      c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) }
79.07/31.65	  Weak Trs:
79.07/31.65	    { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	    , mul0(Nil(), y) -> Nil()
79.07/31.65	    , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	    , add0(Nil(), y) -> y }
79.07/31.65	  Obligation:
79.07/31.65	    innermost runtime complexity
79.07/31.65	  Answer:
79.07/31.65	    YES(O(1),O(1))
79.07/31.65	  
79.07/31.65	  The following weak DPs constitute a sub-graph of the DG that is
79.07/31.65	  closed under successors. The DPs are removed.
79.07/31.65	  
79.07/31.65	  { mul0^#(Cons(x, xs), y) ->
79.07/31.65	    c_1(add0^#(mul0(xs, y), y), mul0^#(xs, y)) }
79.07/31.65	  
79.07/31.65	  We are left with following problem, upon which TcT provides the
79.07/31.65	  certificate YES(O(1),O(1)).
79.07/31.65	  
79.07/31.65	  Weak Trs:
79.07/31.65	    { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	    , mul0(Nil(), y) -> Nil()
79.07/31.65	    , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	    , add0(Nil(), y) -> y }
79.07/31.65	  Obligation:
79.07/31.65	    innermost runtime complexity
79.07/31.65	  Answer:
79.07/31.65	    YES(O(1),O(1))
79.07/31.65	  
79.07/31.65	  No rule is usable, rules are removed from the input problem.
79.07/31.65	  
79.07/31.65	  We are left with following problem, upon which TcT provides the
79.07/31.65	  certificate YES(O(1),O(1)).
79.07/31.65	  
79.07/31.65	  Rules: Empty
79.07/31.65	  Obligation:
79.07/31.65	    innermost runtime complexity
79.07/31.65	  Answer:
79.07/31.65	    YES(O(1),O(1))
79.07/31.65	  
79.07/31.65	  Empty rules are trivially bounded
79.07/31.65	
79.07/31.65	We return to the main proof.
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(n^2)).
79.07/31.65	
79.07/31.65	Strict DPs:
79.07/31.65	  { add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) }
79.07/31.65	Weak DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) -> mul0^#(xs, y)
79.07/31.65	  , mul0^#(Cons(x, xs), y) -> add0^#(mul0(xs, y), y) }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(n^2))
79.07/31.65	
79.07/31.65	We use the processor 'polynomial interpretation' to orient
79.07/31.65	following rules strictly.
79.07/31.65	
79.07/31.65	DPs:
79.07/31.65	  { 1: add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y)))
79.07/31.65	  , 3: mul0^#(Cons(x, xs), y) -> add0^#(mul0(xs, y), y) }
79.07/31.65	
79.07/31.65	Sub-proof:
79.07/31.65	----------
79.07/31.65	  We consider the following typing:
79.07/31.65	  
79.07/31.65	    mul0 :: (b,b) -> b
79.07/31.65	    Cons :: (a,b) -> b
79.07/31.65	    add0 :: (b,b) -> b
79.07/31.65	    S :: a
79.07/31.65	    Nil :: b
79.07/31.65	    mul0^# :: (b,b) -> c
79.07/31.65	    add0^# :: (b,b) -> c
79.07/31.65	    c_3 :: c -> c
79.07/31.65	  
79.07/31.65	  The following argument positions are considered usable:
79.07/31.65	  
79.07/31.65	    Uargs(c_3) = {1}
79.07/31.65	  
79.07/31.65	  TcT has computed the following constructor-restricted
79.07/31.65	  typedpolynomial interpretation.
79.07/31.65	  
79.07/31.65	    [mul0](x1, x2) = x1*x2                      
79.07/31.65	                                                
79.07/31.65	    [Cons](x1, x2) = 1 + x2                     
79.07/31.65	                                                
79.07/31.65	    [add0](x1, x2) = x1 + x2                    
79.07/31.65	                                                
79.07/31.65	             [S]() = 0                          
79.07/31.65	                                                
79.07/31.65	           [Nil]() = 0                          
79.07/31.65	                                                
79.07/31.65	  [mul0^#](x1, x2) = 3 + 3*x1*x2 + 2*x2 + 3*x2^2
79.07/31.65	                                                
79.07/31.65	  [add0^#](x1, x2) = 2*x1                       
79.07/31.65	                                                
79.07/31.65	         [c_3](x1) = x1                         
79.07/31.65	                                                
79.07/31.65	  
79.07/31.65	  This order satisfies the following ordering constraints.
79.07/31.65	  
79.07/31.65	      [mul0(Cons(x, xs), y)] =  y + xs*y                       
79.07/31.65	                             >= xs*y + y                       
79.07/31.65	                             =  [add0(mul0(xs, y), y)]         
79.07/31.65	                                                               
79.07/31.65	            [mul0(Nil(), y)] =                                 
79.07/31.65	                             >=                                
79.07/31.65	                             =  [Nil()]                        
79.07/31.65	                                                               
79.07/31.65	      [add0(Cons(x, xs), y)] =  1 + xs + y                     
79.07/31.65	                             >= xs + 1 + y                     
79.07/31.65	                             =  [add0(xs, Cons(S(), y))]       
79.07/31.65	                                                               
79.07/31.65	            [add0(Nil(), y)] =  y                              
79.07/31.65	                             >= y                              
79.07/31.65	                             =  [y]                            
79.07/31.65	                                                               
79.07/31.65	    [mul0^#(Cons(x, xs), y)] =  3 + 5*y + 3*xs*y + 3*y^2       
79.07/31.65	                             >= 3 + 3*xs*y + 2*y + 3*y^2       
79.07/31.65	                             =  [mul0^#(xs, y)]                
79.07/31.65	                                                               
79.07/31.65	    [mul0^#(Cons(x, xs), y)] =  3 + 5*y + 3*xs*y + 3*y^2       
79.07/31.65	                             >  2*xs*y                         
79.07/31.65	                             =  [add0^#(mul0(xs, y), y)]       
79.07/31.65	                                                               
79.07/31.65	    [add0^#(Cons(x, xs), y)] =  2 + 2*xs                       
79.07/31.65	                             >  2*xs                           
79.07/31.65	                             =  [c_3(add0^#(xs, Cons(S(), y)))]
79.07/31.65	                                                               
79.07/31.65	
79.07/31.65	The strictly oriented rules are moved into the weak component.
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(1)).
79.07/31.65	
79.07/31.65	Weak DPs:
79.07/31.65	  { mul0^#(Cons(x, xs), y) -> mul0^#(xs, y)
79.07/31.65	  , mul0^#(Cons(x, xs), y) -> add0^#(mul0(xs, y), y)
79.07/31.65	  , add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) }
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(1))
79.07/31.65	
79.07/31.65	The following weak DPs constitute a sub-graph of the DG that is
79.07/31.65	closed under successors. The DPs are removed.
79.07/31.65	
79.07/31.65	{ mul0^#(Cons(x, xs), y) -> mul0^#(xs, y)
79.07/31.65	, mul0^#(Cons(x, xs), y) -> add0^#(mul0(xs, y), y)
79.07/31.65	, add0^#(Cons(x, xs), y) -> c_3(add0^#(xs, Cons(S(), y))) }
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(1)).
79.07/31.65	
79.07/31.65	Weak Trs:
79.07/31.65	  { mul0(Cons(x, xs), y) -> add0(mul0(xs, y), y)
79.07/31.65	  , mul0(Nil(), y) -> Nil()
79.07/31.65	  , add0(Cons(x, xs), y) -> add0(xs, Cons(S(), y))
79.07/31.65	  , add0(Nil(), y) -> y }
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(1))
79.07/31.65	
79.07/31.65	No rule is usable, rules are removed from the input problem.
79.07/31.65	
79.07/31.65	We are left with following problem, upon which TcT provides the
79.07/31.65	certificate YES(O(1),O(1)).
79.07/31.65	
79.07/31.65	Rules: Empty
79.07/31.65	Obligation:
79.07/31.65	  innermost runtime complexity
79.07/31.65	Answer:
79.07/31.65	  YES(O(1),O(1))
79.07/31.65	
79.07/31.65	Empty rules are trivially bounded
79.07/31.65	
79.07/31.65	Hurray, we answered YES(O(1),O(n^3))
79.07/31.67	EOF