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