YES(O(1),O(n^1))
70.49/24.02	YES(O(1),O(n^1))
70.49/24.02	
70.49/24.02	We are left with following problem, upon which TcT provides the
70.49/24.02	certificate YES(O(1),O(n^1)).
70.49/24.02	
70.49/24.02	Strict Trs:
70.49/24.02	  { g(f(x), y) -> f(h(x, y))
70.49/24.02	  , h(x, y) -> g(x, f(y)) }
70.49/24.02	Obligation:
70.49/24.02	  runtime complexity
70.49/24.02	Answer:
70.49/24.02	  YES(O(1),O(n^1))
70.49/24.02	
70.49/24.02	The input is overlay and right-linear. Switching to innermost
70.49/24.02	rewriting.
70.49/24.02	
70.49/24.02	We are left with following problem, upon which TcT provides the
70.49/24.02	certificate YES(O(1),O(n^1)).
70.49/24.02	
70.49/24.02	Strict Trs:
70.49/24.02	  { g(f(x), y) -> f(h(x, y))
70.49/24.02	  , h(x, y) -> g(x, f(y)) }
70.49/24.02	Obligation:
70.49/24.02	  innermost runtime complexity
70.49/24.02	Answer:
70.49/24.02	  YES(O(1),O(n^1))
70.49/24.02	
70.49/24.02	The weightgap principle applies (using the following nonconstant
70.49/24.02	growth matrix-interpretation)
70.49/24.02	
70.49/24.02	The following argument positions are usable:
70.49/24.02	  Uargs(f) = {1}
70.49/24.02	
70.49/24.02	TcT has computed the following matrix interpretation satisfying
70.49/24.02	not(EDA) and not(IDA(1)).
70.49/24.02	
70.49/24.02	  [g](x1, x2) = [1] x1 + [1] x2 + [0]
70.49/24.02	                                     
70.49/24.02	      [f](x1) = [1] x1 + [0]         
70.49/24.02	                                     
70.49/24.02	  [h](x1, x2) = [1] x1 + [1] x2 + [1]
70.49/24.02	
70.49/24.02	The order satisfies the following ordering constraints:
70.49/24.02	
70.49/24.02	  [g(f(x), y)] = [1] x + [1] y + [0]
70.49/24.02	               ? [1] x + [1] y + [1]
70.49/24.02	               = [f(h(x, y))]       
70.49/24.02	                                    
70.49/24.02	     [h(x, y)] = [1] x + [1] y + [1]
70.49/24.02	               > [1] x + [1] y + [0]
70.49/24.02	               = [g(x, f(y))]       
70.49/24.02	                                    
70.49/24.02	
70.49/24.02	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
70.49/24.02	
70.49/24.02	We are left with following problem, upon which TcT provides the
70.49/24.02	certificate YES(O(1),O(n^1)).
70.49/24.02	
70.49/24.02	Strict Trs: { g(f(x), y) -> f(h(x, y)) }
70.49/24.02	Weak Trs: { h(x, y) -> g(x, f(y)) }
70.49/24.02	Obligation:
70.49/24.02	  innermost runtime complexity
70.49/24.02	Answer:
70.49/24.02	  YES(O(1),O(n^1))
70.49/24.02	
70.49/24.02	We use the processor 'matrix interpretation of dimension 1' to
70.49/24.02	orient following rules strictly.
70.49/24.02	
70.49/24.02	Trs: { g(f(x), y) -> f(h(x, y)) }
70.49/24.02	
70.49/24.02	The induced complexity on above rules (modulo remaining rules) is
70.49/24.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
70.49/24.02	component(s).
70.49/24.02	
70.49/24.02	Sub-proof:
70.49/24.02	----------
70.49/24.02	  The following argument positions are usable:
70.49/24.02	    Uargs(f) = {1}
70.49/24.02	  
70.49/24.02	  TcT has computed the following constructor-based matrix
70.49/24.02	  interpretation satisfying not(EDA).
70.49/24.02	  
70.49/24.02	    [g](x1, x2) = [2] x1 + [4]
70.49/24.02	                              
70.49/24.02	        [f](x1) = [1] x1 + [4]
70.49/24.02	                              
70.49/24.02	    [h](x1, x2) = [2] x1 + [4]
70.49/24.02	  
70.49/24.02	  The order satisfies the following ordering constraints:
70.49/24.02	  
70.49/24.02	    [g(f(x), y)] =  [2] x + [12]
70.49/24.02	                 >  [2] x + [8] 
70.49/24.02	                 =  [f(h(x, y))]
70.49/24.02	                                
70.49/24.02	       [h(x, y)] =  [2] x + [4] 
70.49/24.02	                 >= [2] x + [4] 
70.49/24.02	                 =  [g(x, f(y))]
70.49/24.02	                                
70.49/24.02	
70.49/24.02	We return to the main proof.
70.49/24.02	
70.49/24.02	We are left with following problem, upon which TcT provides the
70.49/24.02	certificate YES(O(1),O(1)).
70.49/24.02	
70.49/24.02	Weak Trs:
70.49/24.02	  { g(f(x), y) -> f(h(x, y))
70.49/24.02	  , h(x, y) -> g(x, f(y)) }
70.49/24.02	Obligation:
70.49/24.02	  innermost runtime complexity
70.49/24.02	Answer:
70.49/24.02	  YES(O(1),O(1))
70.49/24.02	
70.49/24.02	Empty rules are trivially bounded
70.49/24.02	
70.49/24.02	Hurray, we answered YES(O(1),O(n^1))
70.49/24.02	EOF