YES(O(1),O(1))
8.43/2.53	YES(O(1),O(1))
8.43/2.53	
8.43/2.53	We are left with following problem, upon which TcT provides the
8.43/2.53	certificate YES(O(1),O(1)).
8.43/2.53	
8.43/2.53	Strict Trs:
8.43/2.53	  { +(x, 0()) -> x
8.43/2.53	  , +(x, i(x)) -> 0()
8.43/2.53	  , +(+(x, y), z) -> +(x, +(y, z))
8.43/2.53	  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
8.43/2.53	  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
8.43/2.53	Obligation:
8.43/2.53	  innermost runtime complexity
8.43/2.53	Answer:
8.43/2.53	  YES(O(1),O(1))
8.43/2.53	
8.43/2.53	We add the following dependency tuples:
8.43/2.53	
8.43/2.53	Strict DPs:
8.43/2.53	  { +^#(x, 0()) -> c_1()
8.43/2.53	  , +^#(x, i(x)) -> c_2()
8.43/2.53	  , +^#(+(x, y), z) -> c_3(+^#(x, +(y, z)), +^#(y, z))
8.43/2.53	  , *^#(x, +(y, z)) ->
8.43/2.53	    c_4(+^#(*(x, y), *(x, z)), *^#(x, y), *^#(x, z))
8.43/2.53	  , *^#(+(x, y), z) ->
8.43/2.53	    c_5(+^#(*(x, z), *(y, z)), *^#(x, z), *^#(y, z)) }
8.43/2.53	
8.43/2.53	and mark the set of starting terms.
8.43/2.53	
8.43/2.53	We are left with following problem, upon which TcT provides the
8.43/2.53	certificate YES(O(1),O(1)).
8.43/2.53	
8.43/2.53	Strict DPs:
8.43/2.53	  { +^#(x, 0()) -> c_1()
8.43/2.53	  , +^#(x, i(x)) -> c_2()
8.43/2.53	  , +^#(+(x, y), z) -> c_3(+^#(x, +(y, z)), +^#(y, z))
8.43/2.53	  , *^#(x, +(y, z)) ->
8.43/2.53	    c_4(+^#(*(x, y), *(x, z)), *^#(x, y), *^#(x, z))
8.43/2.53	  , *^#(+(x, y), z) ->
8.43/2.53	    c_5(+^#(*(x, z), *(y, z)), *^#(x, z), *^#(y, z)) }
8.43/2.53	Weak Trs:
8.43/2.53	  { +(x, 0()) -> x
8.43/2.53	  , +(x, i(x)) -> 0()
8.43/2.53	  , +(+(x, y), z) -> +(x, +(y, z))
8.43/2.53	  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
8.43/2.53	  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
8.43/2.53	Obligation:
8.43/2.53	  innermost runtime complexity
8.43/2.53	Answer:
8.43/2.53	  YES(O(1),O(1))
8.43/2.53	
8.43/2.53	Consider the dependency graph:
8.43/2.53	
8.43/2.53	  1: +^#(x, 0()) -> c_1()
8.43/2.53	  
8.43/2.53	  2: +^#(x, i(x)) -> c_2()
8.43/2.53	  
8.43/2.53	  3: +^#(+(x, y), z) -> c_3(+^#(x, +(y, z)), +^#(y, z))
8.43/2.53	     -->_2 +^#(+(x, y), z) -> c_3(+^#(x, +(y, z)), +^#(y, z)) :3
8.43/2.53	     -->_2 +^#(x, i(x)) -> c_2() :2
8.43/2.53	     -->_1 +^#(x, i(x)) -> c_2() :2
8.43/2.53	     -->_2 +^#(x, 0()) -> c_1() :1
8.43/2.53	     -->_1 +^#(x, 0()) -> c_1() :1
8.43/2.53	  
8.43/2.53	  4: *^#(x, +(y, z)) ->
8.43/2.53	     c_4(+^#(*(x, y), *(x, z)), *^#(x, y), *^#(x, z))
8.43/2.53	     -->_3 *^#(+(x, y), z) ->
8.43/2.53	           c_5(+^#(*(x, z), *(y, z)), *^#(x, z), *^#(y, z)) :5
8.43/2.53	     -->_2 *^#(+(x, y), z) ->
8.43/2.53	           c_5(+^#(*(x, z), *(y, z)), *^#(x, z), *^#(y, z)) :5
8.43/2.53	     -->_3 *^#(x, +(y, z)) ->
8.43/2.53	           c_4(+^#(*(x, y), *(x, z)), *^#(x, y), *^#(x, z)) :4
8.43/2.53	     -->_1 +^#(+(x, y), z) -> c_3(+^#(x, +(y, z)), +^#(y, z)) :3
8.43/2.53	     -->_1 +^#(x, i(x)) -> c_2() :2
8.43/2.53	     -->_1 +^#(x, 0()) -> c_1() :1
8.43/2.53	  
8.43/2.53	  5: *^#(+(x, y), z) ->
8.43/2.53	     c_5(+^#(*(x, z), *(y, z)), *^#(x, z), *^#(y, z))
8.43/2.53	     -->_3 *^#(+(x, y), z) ->
8.43/2.53	           c_5(+^#(*(x, z), *(y, z)), *^#(x, z), *^#(y, z)) :5
8.43/2.53	     -->_3 *^#(x, +(y, z)) ->
8.43/2.53	           c_4(+^#(*(x, y), *(x, z)), *^#(x, y), *^#(x, z)) :4
8.43/2.53	     -->_2 *^#(x, +(y, z)) ->
8.43/2.53	           c_4(+^#(*(x, y), *(x, z)), *^#(x, y), *^#(x, z)) :4
8.43/2.53	     -->_1 +^#(+(x, y), z) -> c_3(+^#(x, +(y, z)), +^#(y, z)) :3
8.43/2.53	     -->_1 +^#(x, i(x)) -> c_2() :2
8.43/2.53	     -->_1 +^#(x, 0()) -> c_1() :1
8.43/2.53	  
8.43/2.53	
8.43/2.53	Only the nodes {1,2} are reachable from nodes {1,2} that start
8.43/2.53	derivation from marked basic terms. The nodes not reachable are
8.43/2.53	removed from the problem.
8.43/2.53	
8.43/2.53	We are left with following problem, upon which TcT provides the
8.43/2.53	certificate YES(O(1),O(1)).
8.43/2.53	
8.43/2.53	Strict DPs:
8.43/2.53	  { +^#(x, 0()) -> c_1()
8.43/2.53	  , +^#(x, i(x)) -> c_2() }
8.43/2.53	Weak Trs:
8.43/2.53	  { +(x, 0()) -> x
8.43/2.53	  , +(x, i(x)) -> 0()
8.43/2.53	  , +(+(x, y), z) -> +(x, +(y, z))
8.43/2.53	  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
8.43/2.53	  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
8.43/2.53	Obligation:
8.43/2.53	  innermost runtime complexity
8.43/2.53	Answer:
8.43/2.53	  YES(O(1),O(1))
8.43/2.53	
8.43/2.53	We estimate the number of application of {1,2} by applications of
8.43/2.53	Pre({1,2}) = {}. Here rules are labeled as follows:
8.43/2.53	
8.43/2.53	  DPs:
8.43/2.53	    { 1: +^#(x, 0()) -> c_1()
8.43/2.53	    , 2: +^#(x, i(x)) -> c_2() }
8.43/2.53	
8.43/2.53	We are left with following problem, upon which TcT provides the
8.43/2.53	certificate YES(O(1),O(1)).
8.43/2.53	
8.43/2.53	Weak DPs:
8.43/2.53	  { +^#(x, 0()) -> c_1()
8.43/2.53	  , +^#(x, i(x)) -> c_2() }
8.43/2.53	Weak Trs:
8.43/2.53	  { +(x, 0()) -> x
8.43/2.53	  , +(x, i(x)) -> 0()
8.43/2.53	  , +(+(x, y), z) -> +(x, +(y, z))
8.43/2.53	  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
8.43/2.53	  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
8.43/2.53	Obligation:
8.43/2.53	  innermost runtime complexity
8.43/2.53	Answer:
8.43/2.53	  YES(O(1),O(1))
8.43/2.53	
8.43/2.53	The following weak DPs constitute a sub-graph of the DG that is
8.43/2.53	closed under successors. The DPs are removed.
8.43/2.53	
8.43/2.53	{ +^#(x, 0()) -> c_1()
8.43/2.53	, +^#(x, i(x)) -> c_2() }
8.43/2.53	
8.43/2.53	We are left with following problem, upon which TcT provides the
8.43/2.53	certificate YES(O(1),O(1)).
8.43/2.53	
8.43/2.53	Weak Trs:
8.43/2.53	  { +(x, 0()) -> x
8.43/2.53	  , +(x, i(x)) -> 0()
8.43/2.54	  , +(+(x, y), z) -> +(x, +(y, z))
8.43/2.54	  , *(x, +(y, z)) -> +(*(x, y), *(x, z))
8.43/2.54	  , *(+(x, y), z) -> +(*(x, z), *(y, z)) }
8.43/2.54	Obligation:
8.43/2.54	  innermost runtime complexity
8.43/2.54	Answer:
8.43/2.54	  YES(O(1),O(1))
8.43/2.54	
8.43/2.54	No rule is usable, rules are removed from the input problem.
8.43/2.54	
8.43/2.54	We are left with following problem, upon which TcT provides the
8.43/2.54	certificate YES(O(1),O(1)).
8.43/2.54	
8.43/2.54	Rules: Empty
8.43/2.54	Obligation:
8.43/2.54	  innermost runtime complexity
8.43/2.54	Answer:
8.43/2.54	  YES(O(1),O(1))
8.43/2.54	
8.43/2.54	Empty rules are trivially bounded
8.43/2.54	
8.43/2.54	Hurray, we answered YES(O(1),O(1))
8.43/2.55	EOF