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