YES(O(1),O(n^1))
6.09/3.64	YES(O(1),O(n^1))
6.09/3.64	
6.09/3.64	We are left with following problem, upon which TcT provides the
6.09/3.64	certificate YES(O(1),O(n^1)).
6.09/3.64	
6.09/3.64	Strict Trs: { f(g(x, y), f(y, y)) -> f(g(y, x), y) }
6.09/3.64	Obligation:
6.09/3.64	  derivational complexity
6.09/3.64	Answer:
6.09/3.64	  YES(O(1),O(n^1))
6.09/3.64	
6.09/3.64	We use the processor 'matrix interpretation of dimension 1' to
6.09/3.64	orient following rules strictly.
6.09/3.64	
6.09/3.64	Trs: { f(g(x, y), f(y, y)) -> f(g(y, x), y) }
6.09/3.64	
6.09/3.64	The induced complexity on above rules (modulo remaining rules) is
6.09/3.64	YES(?,O(n^1)) . These rules are moved into the corresponding weak
6.09/3.64	component(s).
6.09/3.64	
6.09/3.64	Sub-proof:
6.09/3.64	----------
6.09/3.64	  TcT has computed the following triangular matrix interpretation.
6.09/3.64	  
6.09/3.64	    [f](x1, x2) = [1] x1 + [1] x2 + [2]
6.09/3.64	                                       
6.09/3.64	    [g](x1, x2) = [1] x1 + [1] x2 + [0]
6.09/3.64	  
6.09/3.64	  The order satisfies the following ordering constraints:
6.09/3.64	  
6.09/3.64	    [f(g(x, y), f(y, y))] = [1] x + [3] y + [4]
6.09/3.64	                          > [1] x + [2] y + [2]
6.09/3.64	                          = [f(g(y, x), y)]    
6.09/3.64	                                               
6.09/3.64	
6.09/3.64	We return to the main proof.
6.09/3.64	
6.09/3.64	We are left with following problem, upon which TcT provides the
6.09/3.64	certificate YES(O(1),O(1)).
6.09/3.64	
6.09/3.64	Weak Trs: { f(g(x, y), f(y, y)) -> f(g(y, x), y) }
6.09/3.64	Obligation:
6.09/3.64	  derivational complexity
6.09/3.64	Answer:
6.09/3.64	  YES(O(1),O(1))
6.09/3.64	
6.09/3.64	Empty rules are trivially bounded
6.09/3.64	
6.09/3.64	Hurray, we answered YES(O(1),O(n^1))
6.09/3.65	EOF