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