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