YES(O(1),O(n^2))
173.66/60.07	YES(O(1),O(n^2))
173.66/60.07	
173.66/60.07	We are left with following problem, upon which TcT provides the
173.66/60.07	certificate YES(O(1),O(n^2)).
173.66/60.07	
173.66/60.07	Strict Trs:
173.66/60.07	  { h(f(x), y) -> f(g(x, y))
173.66/60.07	  , g(x, y) -> h(x, y) }
173.66/60.07	Obligation:
173.66/60.07	  derivational complexity
173.66/60.07	Answer:
173.66/60.07	  YES(O(1),O(n^2))
173.66/60.07	
173.66/60.07	The weightgap principle applies (using the following nonconstant
173.66/60.07	growth matrix-interpretation)
173.66/60.07	
173.66/60.07	TcT has computed the following triangular matrix interpretation.
173.66/60.07	Note that the diagonal of the component-wise maxima of
173.66/60.07	interpretation-entries contains no more than 1 non-zero entries.
173.66/60.07	
173.66/60.07	  [h](x1, x2) = [1] x1 + [1] x2 + [0]
173.66/60.07	                                     
173.66/60.07	      [f](x1) = [1] x1 + [0]         
173.66/60.07	                                     
173.66/60.07	  [g](x1, x2) = [1] x1 + [1] x2 + [1]
173.66/60.07	
173.66/60.07	The order satisfies the following ordering constraints:
173.66/60.07	
173.66/60.07	  [h(f(x), y)] = [1] x + [1] y + [0]
173.66/60.07	               ? [1] x + [1] y + [1]
173.66/60.07	               = [f(g(x, y))]       
173.66/60.07	                                    
173.66/60.07	     [g(x, y)] = [1] x + [1] y + [1]
173.66/60.07	               > [1] x + [1] y + [0]
173.66/60.07	               = [h(x, y)]          
173.66/60.07	                                    
173.66/60.07	
173.66/60.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
173.66/60.07	
173.66/60.07	We are left with following problem, upon which TcT provides the
173.66/60.07	certificate YES(O(1),O(n^2)).
173.66/60.07	
173.66/60.07	Strict Trs: { h(f(x), y) -> f(g(x, y)) }
173.66/60.07	Weak Trs: { g(x, y) -> h(x, y) }
173.66/60.07	Obligation:
173.66/60.07	  derivational complexity
173.66/60.07	Answer:
173.66/60.07	  YES(O(1),O(n^2))
173.66/60.07	
173.66/60.07	We use the processor 'matrix interpretation of dimension 3' to
173.66/60.07	orient following rules strictly.
173.66/60.07	
173.66/60.07	Trs: { h(f(x), y) -> f(g(x, y)) }
173.66/60.07	
173.66/60.07	The induced complexity on above rules (modulo remaining rules) is
173.66/60.07	YES(?,O(n^2)) . These rules are moved into the corresponding weak
173.66/60.07	component(s).
173.66/60.07	
173.66/60.07	Sub-proof:
173.66/60.07	----------
173.66/60.07	  TcT has computed the following triangular matrix interpretation.
173.66/60.07	  Note that the diagonal of the component-wise maxima of
173.66/60.07	  interpretation-entries contains no more than 2 non-zero entries.
173.66/60.07	  
173.66/60.07	                  [1 1 0]      [1 1 1]      [0]
173.66/60.07	    [h](x1, x2) = [0 1 0] x1 + [0 1 2] x2 + [0]
173.66/60.07	                  [0 0 0]      [0 0 0]      [0]
173.66/60.07	                                               
173.66/60.07	                  [1 0 0]      [0]             
173.66/60.07	        [f](x1) = [0 1 0] x1 + [1]             
173.66/60.07	                  [0 0 0]      [0]             
173.66/60.07	                                               
173.66/60.07	                  [1 1 0]      [1 1 1]      [0]
173.66/60.07	    [g](x1, x2) = [0 1 0] x1 + [0 1 2] x2 + [0]
173.66/60.07	                  [0 0 0]      [0 0 0]      [0]
173.66/60.07	  
173.66/60.07	  The order satisfies the following ordering constraints:
173.66/60.07	  
173.66/60.07	    [h(f(x), y)] =  [1 1 0]     [1 1 1]     [1]
173.66/60.07	                    [0 1 0] x + [0 1 2] y + [1]
173.66/60.07	                    [0 0 0]     [0 0 0]     [0]
173.66/60.07	                 >  [1 1 0]     [1 1 1]     [0]
173.66/60.07	                    [0 1 0] x + [0 1 2] y + [1]
173.66/60.07	                    [0 0 0]     [0 0 0]     [0]
173.66/60.07	                 =  [f(g(x, y))]               
173.66/60.07	                                               
173.66/60.07	       [g(x, y)] =  [1 1 0]     [1 1 1]     [0]
173.66/60.07	                    [0 1 0] x + [0 1 2] y + [0]
173.66/60.07	                    [0 0 0]     [0 0 0]     [0]
173.66/60.07	                 >= [1 1 0]     [1 1 1]     [0]
173.66/60.07	                    [0 1 0] x + [0 1 2] y + [0]
173.66/60.07	                    [0 0 0]     [0 0 0]     [0]
173.66/60.07	                 =  [h(x, y)]                  
173.66/60.07	                                               
173.66/60.07	
173.66/60.07	We return to the main proof.
173.66/60.07	
173.66/60.07	We are left with following problem, upon which TcT provides the
173.66/60.07	certificate YES(O(1),O(1)).
173.66/60.07	
173.66/60.07	Weak Trs:
173.66/60.07	  { h(f(x), y) -> f(g(x, y))
173.66/60.07	  , g(x, y) -> h(x, y) }
173.66/60.07	Obligation:
173.66/60.07	  derivational complexity
173.66/60.07	Answer:
173.66/60.07	  YES(O(1),O(1))
173.66/60.07	
173.66/60.07	Empty rules are trivially bounded
173.66/60.07	
173.66/60.07	Hurray, we answered YES(O(1),O(n^2))
173.66/60.07	EOF