YES(O(1),O(n^2))
186.31/60.07	YES(O(1),O(n^2))
186.31/60.07	
186.31/60.07	We are left with following problem, upon which TcT provides the
186.31/60.07	certificate YES(O(1),O(n^2)).
186.31/60.07	
186.31/60.07	Strict Trs:
186.31/60.07	  { rev(a()) -> a()
186.31/60.07	  , rev(b()) -> b()
186.31/60.07	  , rev(++(x, x)) -> rev(x)
186.31/60.07	  , rev(++(x, y)) -> ++(rev(y), rev(x)) }
186.31/60.07	Obligation:
186.31/60.07	  derivational complexity
186.31/60.07	Answer:
186.31/60.07	  YES(O(1),O(n^2))
186.31/60.07	
186.31/60.07	We use the processor 'matrix interpretation of dimension 2' to
186.31/60.07	orient following rules strictly.
186.31/60.07	
186.31/60.07	Trs:
186.31/60.07	  { rev(a()) -> a()
186.31/60.07	  , rev(b()) -> b()
186.31/60.07	  , rev(++(x, x)) -> rev(x)
186.31/60.07	  , rev(++(x, y)) -> ++(rev(y), rev(x)) }
186.31/60.07	
186.31/60.07	The induced complexity on above rules (modulo remaining rules) is
186.31/60.07	YES(?,O(n^2)) . These rules are removed from the problem. Note that
186.31/60.07	none of the weakly oriented rules is size-increasing. The overall
186.31/60.07	complexity is obtained by composition .
186.31/60.07	
186.31/60.07	Sub-proof:
186.31/60.07	----------
186.31/60.07	  TcT has computed the following triangular matrix interpretation.
186.31/60.07	  
186.31/60.07	       [rev](x1) = [1 2] x1 + [0]           
186.31/60.07	                   [0 1]      [0]           
186.31/60.07	                                            
186.31/60.07	             [a] = [2]                      
186.31/60.07	                   [1]                      
186.31/60.07	                                            
186.31/60.07	             [b] = [0]                      
186.31/60.07	                   [2]                      
186.31/60.07	                                            
186.31/60.07	    [++](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
186.31/60.07	                   [0 1]      [0 1]      [1]
186.31/60.07	  
186.31/60.07	  The order satisfies the following ordering constraints:
186.31/60.07	  
186.31/60.07	         [rev(a())] = [4]                    
186.31/60.07	                      [1]                    
186.31/60.07	                    > [2]                    
186.31/60.07	                      [1]                    
186.31/60.07	                    = [a()]                  
186.31/60.07	                                             
186.31/60.07	         [rev(b())] = [4]                    
186.31/60.07	                      [2]                    
186.31/60.07	                    > [0]                    
186.31/60.07	                      [2]                    
186.31/60.07	                    = [b()]                  
186.31/60.07	                                             
186.31/60.07	    [rev(++(x, x))] = [2 4] x + [2]          
186.31/60.07	                      [0 2]     [1]          
186.31/60.07	                    > [1 2] x + [0]          
186.31/60.07	                      [0 1]     [0]          
186.31/60.07	                    = [rev(x)]               
186.31/60.07	                                             
186.31/60.07	    [rev(++(x, y))] = [1 2] x + [1 2] y + [2]
186.31/60.07	                      [0 1]     [0 1]     [1]
186.31/60.07	                    > [1 2] x + [1 2] y + [0]
186.31/60.07	                      [0 1]     [0 1]     [1]
186.31/60.07	                    = [++(rev(y), rev(x))]   
186.31/60.07	                                             
186.31/60.07	
186.31/60.07	We return to the main proof.
186.31/60.07	
186.31/60.07	We are left with following problem, upon which TcT provides the
186.31/60.07	certificate YES(O(1),O(1)).
186.31/60.07	
186.31/60.07	Rules: Empty
186.31/60.07	Obligation:
186.31/60.07	  derivational complexity
186.31/60.07	Answer:
186.31/60.07	  YES(O(1),O(1))
186.31/60.07	
186.31/60.07	Empty rules are trivially bounded
186.31/60.07	
186.31/60.07	Hurray, we answered YES(O(1),O(n^2))
186.31/60.07	EOF