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