YES(O(1),O(n^1))
6.63/2.03	YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(n^1)).
6.63/2.03	
6.63/2.03	Strict Trs:
6.63/2.03	  { f(x, 0()) -> x
6.63/2.03	  , f(f(x, y), z) -> f(x, f(y, z))
6.63/2.03	  , f(0(), y) -> y
6.63/2.03	  , f(i(x), y) -> i(x)
6.63/2.03	  , f(g(x, y), z) -> g(f(x, z), f(y, z))
6.63/2.03	  , f(1(), g(x, y)) -> x
6.63/2.03	  , f(2(), g(x, y)) -> y }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	We add the following dependency tuples:
6.63/2.03	
6.63/2.03	Strict DPs:
6.63/2.03	  { f^#(x, 0()) -> c_1()
6.63/2.03	  , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z)), f^#(y, z))
6.63/2.03	  , f^#(0(), y) -> c_3()
6.63/2.03	  , f^#(i(x), y) -> c_4()
6.63/2.03	  , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z))
6.63/2.03	  , f^#(1(), g(x, y)) -> c_6()
6.63/2.03	  , f^#(2(), g(x, y)) -> c_7() }
6.63/2.03	
6.63/2.03	and mark the set of starting terms.
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(n^1)).
6.63/2.03	
6.63/2.03	Strict DPs:
6.63/2.03	  { f^#(x, 0()) -> c_1()
6.63/2.03	  , f^#(f(x, y), z) -> c_2(f^#(x, f(y, z)), f^#(y, z))
6.63/2.03	  , f^#(0(), y) -> c_3()
6.63/2.03	  , f^#(i(x), y) -> c_4()
6.63/2.03	  , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z))
6.63/2.03	  , f^#(1(), g(x, y)) -> c_6()
6.63/2.03	  , f^#(2(), g(x, y)) -> c_7() }
6.63/2.03	Weak Trs:
6.63/2.03	  { f(x, 0()) -> x
6.63/2.03	  , f(f(x, y), z) -> f(x, f(y, z))
6.63/2.03	  , f(0(), y) -> y
6.63/2.03	  , f(i(x), y) -> i(x)
6.63/2.03	  , f(g(x, y), z) -> g(f(x, z), f(y, z))
6.63/2.03	  , f(1(), g(x, y)) -> x
6.63/2.03	  , f(2(), g(x, y)) -> y }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	We estimate the number of application of {1,3,4,6,7} by
6.63/2.03	applications of Pre({1,3,4,6,7}) = {2,5}. Here rules are labeled as
6.63/2.03	follows:
6.63/2.03	
6.63/2.03	  DPs:
6.63/2.03	    { 1: f^#(x, 0()) -> c_1()
6.63/2.03	    , 2: f^#(f(x, y), z) -> c_2(f^#(x, f(y, z)), f^#(y, z))
6.63/2.03	    , 3: f^#(0(), y) -> c_3()
6.63/2.03	    , 4: f^#(i(x), y) -> c_4()
6.63/2.03	    , 5: f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z))
6.63/2.03	    , 6: f^#(1(), g(x, y)) -> c_6()
6.63/2.03	    , 7: f^#(2(), g(x, y)) -> c_7() }
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(n^1)).
6.63/2.03	
6.63/2.03	Strict DPs:
6.63/2.03	  { f^#(f(x, y), z) -> c_2(f^#(x, f(y, z)), f^#(y, z))
6.63/2.03	  , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) }
6.63/2.03	Weak DPs:
6.63/2.03	  { f^#(x, 0()) -> c_1()
6.63/2.03	  , f^#(0(), y) -> c_3()
6.63/2.03	  , f^#(i(x), y) -> c_4()
6.63/2.03	  , f^#(1(), g(x, y)) -> c_6()
6.63/2.03	  , f^#(2(), g(x, y)) -> c_7() }
6.63/2.03	Weak Trs:
6.63/2.03	  { f(x, 0()) -> x
6.63/2.03	  , f(f(x, y), z) -> f(x, f(y, z))
6.63/2.03	  , f(0(), y) -> y
6.63/2.03	  , f(i(x), y) -> i(x)
6.63/2.03	  , f(g(x, y), z) -> g(f(x, z), f(y, z))
6.63/2.03	  , f(1(), g(x, y)) -> x
6.63/2.03	  , f(2(), g(x, y)) -> y }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	The following weak DPs constitute a sub-graph of the DG that is
6.63/2.03	closed under successors. The DPs are removed.
6.63/2.03	
6.63/2.03	{ f^#(x, 0()) -> c_1()
6.63/2.03	, f^#(0(), y) -> c_3()
6.63/2.03	, f^#(i(x), y) -> c_4()
6.63/2.03	, f^#(1(), g(x, y)) -> c_6()
6.63/2.03	, f^#(2(), g(x, y)) -> c_7() }
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(n^1)).
6.63/2.03	
6.63/2.03	Strict DPs:
6.63/2.03	  { f^#(f(x, y), z) -> c_2(f^#(x, f(y, z)), f^#(y, z))
6.63/2.03	  , f^#(g(x, y), z) -> c_5(f^#(x, z), f^#(y, z)) }
6.63/2.03	Weak Trs:
6.63/2.03	  { f(x, 0()) -> x
6.63/2.03	  , f(f(x, y), z) -> f(x, f(y, z))
6.63/2.03	  , f(0(), y) -> y
6.63/2.03	  , f(i(x), y) -> i(x)
6.63/2.03	  , f(g(x, y), z) -> g(f(x, z), f(y, z))
6.63/2.03	  , f(1(), g(x, y)) -> x
6.63/2.03	  , f(2(), g(x, y)) -> y }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	Due to missing edges in the dependency-graph, the right-hand sides
6.63/2.03	of following rules could be simplified:
6.63/2.03	
6.63/2.03	  { f^#(f(x, y), z) -> c_2(f^#(x, f(y, z)), f^#(y, z)) }
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(n^1)).
6.63/2.03	
6.63/2.03	Strict DPs:
6.63/2.03	  { f^#(f(x, y), z) -> c_1(f^#(y, z))
6.63/2.03	  , f^#(g(x, y), z) -> c_2(f^#(x, z), f^#(y, z)) }
6.63/2.03	Weak Trs:
6.63/2.03	  { f(x, 0()) -> x
6.63/2.03	  , f(f(x, y), z) -> f(x, f(y, z))
6.63/2.03	  , f(0(), y) -> y
6.63/2.03	  , f(i(x), y) -> i(x)
6.63/2.03	  , f(g(x, y), z) -> g(f(x, z), f(y, z))
6.63/2.03	  , f(1(), g(x, y)) -> x
6.63/2.03	  , f(2(), g(x, y)) -> y }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	No rule is usable, rules are removed from the input problem.
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(n^1)).
6.63/2.03	
6.63/2.03	Strict DPs:
6.63/2.03	  { f^#(f(x, y), z) -> c_1(f^#(y, z))
6.63/2.03	  , f^#(g(x, y), z) -> c_2(f^#(x, z), f^#(y, z)) }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(n^1))
6.63/2.03	
6.63/2.03	We use the processor 'matrix interpretation of dimension 1' to
6.63/2.03	orient following rules strictly.
6.63/2.03	
6.63/2.03	DPs:
6.63/2.03	  { 1: f^#(f(x, y), z) -> c_1(f^#(y, z))
6.63/2.03	  , 2: f^#(g(x, y), z) -> c_2(f^#(x, z), f^#(y, z)) }
6.63/2.03	
6.63/2.03	Sub-proof:
6.63/2.03	----------
6.63/2.03	  The following argument positions are usable:
6.63/2.03	    Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}
6.63/2.03	  
6.63/2.03	  TcT has computed the following constructor-based matrix
6.63/2.03	  interpretation satisfying not(EDA).
6.63/2.03	  
6.63/2.03	      [f](x1, x2) = [7] x1 + [2] x2 + [2]
6.63/2.03	                                         
6.63/2.03	      [g](x1, x2) = [1] x1 + [1] x2 + [2]
6.63/2.03	                                         
6.63/2.03	    [f^#](x1, x2) = [4] x1 + [0]         
6.63/2.03	                                         
6.63/2.03	        [c_1](x1) = [1] x1 + [3]         
6.63/2.03	                                         
6.63/2.03	    [c_2](x1, x2) = [1] x1 + [1] x2 + [1]
6.63/2.03	  
6.63/2.03	  The order satisfies the following ordering constraints:
6.63/2.03	  
6.63/2.03	    [f^#(f(x, y), z)] = [8] y + [28] x + [8]       
6.63/2.03	                      > [4] y + [3]                
6.63/2.03	                      = [c_1(f^#(y, z))]           
6.63/2.03	                                                   
6.63/2.03	    [f^#(g(x, y), z)] = [4] y + [4] x + [8]        
6.63/2.03	                      > [4] y + [4] x + [1]        
6.63/2.03	                      = [c_2(f^#(x, z), f^#(y, z))]
6.63/2.03	                                                   
6.63/2.03	
6.63/2.03	The strictly oriented rules are moved into the weak component.
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(1)).
6.63/2.03	
6.63/2.03	Weak DPs:
6.63/2.03	  { f^#(f(x, y), z) -> c_1(f^#(y, z))
6.63/2.03	  , f^#(g(x, y), z) -> c_2(f^#(x, z), f^#(y, z)) }
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(1))
6.63/2.03	
6.63/2.03	The following weak DPs constitute a sub-graph of the DG that is
6.63/2.03	closed under successors. The DPs are removed.
6.63/2.03	
6.63/2.03	{ f^#(f(x, y), z) -> c_1(f^#(y, z))
6.63/2.03	, f^#(g(x, y), z) -> c_2(f^#(x, z), f^#(y, z)) }
6.63/2.03	
6.63/2.03	We are left with following problem, upon which TcT provides the
6.63/2.03	certificate YES(O(1),O(1)).
6.63/2.03	
6.63/2.03	Rules: Empty
6.63/2.03	Obligation:
6.63/2.03	  innermost runtime complexity
6.63/2.03	Answer:
6.63/2.03	  YES(O(1),O(1))
6.63/2.03	
6.63/2.03	Empty rules are trivially bounded
6.63/2.03	
6.63/2.03	Hurray, we answered YES(O(1),O(n^1))
6.63/2.03	EOF