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