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