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