YES(O(1),O(n^1))
239.71/67.51	YES(O(1),O(n^1))
239.71/67.51	
239.71/67.51	We are left with following problem, upon which TcT provides the
239.71/67.51	certificate YES(O(1),O(n^1)).
239.71/67.51	
239.71/67.51	Strict Trs:
239.71/67.51	  { a(x1) -> b(x1)
239.71/67.51	  , a(a(x1)) -> a(b(a(x1)))
239.71/67.51	  , a(a(a(x1))) -> a(a(b(a(a(x1)))))
239.71/67.51	  , a(a(b(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , a(b(x1)) -> b(b(b(x1)))
239.71/67.51	  , a(b(a(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , a(b(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.51	  , a(b(b(x1))) -> b(b(b(b(b(x1)))))
239.71/67.51	  , b(a(x1)) -> b(b(b(x1)))
239.71/67.51	  , b(a(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.51	  , b(b(a(x1))) -> b(b(b(b(b(x1))))) }
239.71/67.51	Obligation:
239.71/67.51	  derivational complexity
239.71/67.51	Answer:
239.71/67.51	  YES(O(1),O(n^1))
239.71/67.51	
239.71/67.51	The weightgap principle applies (using the following nonconstant
239.71/67.51	growth matrix-interpretation)
239.71/67.51	
239.71/67.51	TcT has computed the following triangular matrix interpretation.
239.71/67.51	Note that the diagonal of the component-wise maxima of
239.71/67.51	interpretation-entries contains no more than 1 non-zero entries.
239.71/67.51	
239.71/67.51	  [a](x1) = [1] x1 + [1]
239.71/67.51	                        
239.71/67.51	  [b](x1) = [1] x1 + [0]
239.71/67.51	
239.71/67.51	The order satisfies the following ordering constraints:
239.71/67.51	
239.71/67.51	        [a(x1)] =  [1] x1 + [1]       
239.71/67.51	                >  [1] x1 + [0]       
239.71/67.51	                =  [b(x1)]            
239.71/67.51	                                      
239.71/67.51	     [a(a(x1))] =  [1] x1 + [2]       
239.71/67.51	                >= [1] x1 + [2]       
239.71/67.51	                =  [a(b(a(x1)))]      
239.71/67.51	                                      
239.71/67.51	  [a(a(a(x1)))] =  [1] x1 + [3]       
239.71/67.51	                ?  [1] x1 + [4]       
239.71/67.51	                =  [a(a(b(a(a(x1)))))]
239.71/67.51	                                      
239.71/67.51	  [a(a(b(x1)))] =  [1] x1 + [2]       
239.71/67.51	                >= [1] x1 + [2]       
239.71/67.51	                =  [a(b(b(a(b(x1)))))]
239.71/67.51	                                      
239.71/67.51	     [a(b(x1))] =  [1] x1 + [1]       
239.71/67.51	                >  [1] x1 + [0]       
239.71/67.51	                =  [b(b(b(x1)))]      
239.71/67.51	                                      
239.71/67.51	  [a(b(a(x1)))] =  [1] x1 + [2]       
239.71/67.51	                >= [1] x1 + [2]       
239.71/67.51	                =  [a(b(b(a(b(x1)))))]
239.71/67.51	                                      
239.71/67.51	  [a(b(a(x1)))] =  [1] x1 + [2]       
239.71/67.51	                >= [1] x1 + [2]       
239.71/67.51	                =  [b(a(b(b(a(x1)))))]
239.71/67.51	                                      
239.71/67.51	  [a(b(b(x1)))] =  [1] x1 + [1]       
239.71/67.51	                >  [1] x1 + [0]       
239.71/67.51	                =  [b(b(b(b(b(x1)))))]
239.71/67.51	                                      
239.71/67.51	     [b(a(x1))] =  [1] x1 + [1]       
239.71/67.51	                >  [1] x1 + [0]       
239.71/67.51	                =  [b(b(b(x1)))]      
239.71/67.51	                                      
239.71/67.51	  [b(a(a(x1)))] =  [1] x1 + [2]       
239.71/67.51	                >= [1] x1 + [2]       
239.71/67.51	                =  [b(a(b(b(a(x1)))))]
239.71/67.51	                                      
239.71/67.51	  [b(b(a(x1)))] =  [1] x1 + [1]       
239.71/67.51	                >  [1] x1 + [0]       
239.71/67.51	                =  [b(b(b(b(b(x1)))))]
239.71/67.51	                                      
239.71/67.51	
239.71/67.51	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
239.71/67.51	
239.71/67.51	We are left with following problem, upon which TcT provides the
239.71/67.51	certificate YES(O(1),O(n^1)).
239.71/67.51	
239.71/67.51	Strict Trs:
239.71/67.51	  { a(a(x1)) -> a(b(a(x1)))
239.71/67.51	  , a(a(a(x1))) -> a(a(b(a(a(x1)))))
239.71/67.51	  , a(a(b(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , a(b(a(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , a(b(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.51	  , b(a(a(x1))) -> b(a(b(b(a(x1))))) }
239.71/67.51	Weak Trs:
239.71/67.51	  { a(x1) -> b(x1)
239.71/67.51	  , a(b(x1)) -> b(b(b(x1)))
239.71/67.51	  , a(b(b(x1))) -> b(b(b(b(b(x1)))))
239.71/67.51	  , b(a(x1)) -> b(b(b(x1)))
239.71/67.51	  , b(b(a(x1))) -> b(b(b(b(b(x1))))) }
239.71/67.51	Obligation:
239.71/67.51	  derivational complexity
239.71/67.51	Answer:
239.71/67.51	  YES(O(1),O(n^1))
239.71/67.51	
239.71/67.51	We use the processor 'matrix interpretation of dimension 3' to
239.71/67.51	orient following rules strictly.
239.71/67.51	
239.71/67.51	Trs:
239.71/67.51	  { a(a(x1)) -> a(b(a(x1)))
239.71/67.51	  , a(a(b(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , b(a(a(x1))) -> b(a(b(b(a(x1))))) }
239.71/67.51	
239.71/67.51	The induced complexity on above rules (modulo remaining rules) is
239.71/67.51	YES(?,O(n^1)) . These rules are moved into the corresponding weak
239.71/67.51	component(s).
239.71/67.51	
239.71/67.51	Sub-proof:
239.71/67.51	----------
239.71/67.51	  TcT has computed the following triangular matrix interpretation.
239.71/67.51	  Note that the diagonal of the component-wise maxima of
239.71/67.51	  interpretation-entries contains no more than 1 non-zero entries.
239.71/67.51	  
239.71/67.51	              [1 0 1]      [0]
239.71/67.51	    [a](x1) = [0 0 0] x1 + [0]
239.71/67.51	              [0 0 0]      [1]
239.71/67.51	                              
239.71/67.51	              [1 0 0]      [0]
239.71/67.51	    [b](x1) = [0 0 0] x1 + [0]
239.71/67.51	              [0 0 0]      [0]
239.71/67.51	  
239.71/67.51	  The order satisfies the following ordering constraints:
239.71/67.51	  
239.71/67.51	          [a(x1)] =  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(x1)]            
239.71/67.51	                                        
239.71/67.51	       [a(a(x1))] =  [1 0 1]      [1]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  =  [a(b(a(x1)))]      
239.71/67.51	                                        
239.71/67.51	    [a(a(a(x1)))] =  [1 0 1]      [2]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 1]      [2]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  =  [a(a(b(a(a(x1)))))]
239.71/67.51	                                        
239.71/67.51	    [a(a(b(x1)))] =  [1 0 0]      [1]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >  [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  =  [a(b(b(a(b(x1)))))]
239.71/67.51	                                        
239.71/67.51	       [a(b(x1))] =  [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(b(b(x1)))]      
239.71/67.51	                                        
239.71/67.51	    [a(b(a(x1)))] =  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  =  [a(b(b(a(b(x1)))))]
239.71/67.51	                                        
239.71/67.51	    [a(b(a(x1)))] =  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(a(b(b(a(x1)))))]
239.71/67.51	                                        
239.71/67.51	    [a(b(b(x1)))] =  [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(b(b(b(b(x1)))))]
239.71/67.51	                                        
239.71/67.51	       [b(a(x1))] =  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(b(b(x1)))]      
239.71/67.51	                                        
239.71/67.51	    [b(a(a(x1)))] =  [1 0 1]      [1]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  >  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(a(b(b(a(x1)))))]
239.71/67.51	                                        
239.71/67.51	    [b(b(a(x1)))] =  [1 0 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(b(b(b(b(x1)))))]
239.71/67.51	                                        
239.71/67.51	
239.71/67.51	We return to the main proof.
239.71/67.51	
239.71/67.51	We are left with following problem, upon which TcT provides the
239.71/67.51	certificate YES(O(1),O(n^1)).
239.71/67.51	
239.71/67.51	Strict Trs:
239.71/67.51	  { a(a(a(x1))) -> a(a(b(a(a(x1)))))
239.71/67.51	  , a(b(a(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , a(b(a(x1))) -> b(a(b(b(a(x1))))) }
239.71/67.51	Weak Trs:
239.71/67.51	  { a(x1) -> b(x1)
239.71/67.51	  , a(a(x1)) -> a(b(a(x1)))
239.71/67.51	  , a(a(b(x1))) -> a(b(b(a(b(x1)))))
239.71/67.51	  , a(b(x1)) -> b(b(b(x1)))
239.71/67.51	  , a(b(b(x1))) -> b(b(b(b(b(x1)))))
239.71/67.51	  , b(a(x1)) -> b(b(b(x1)))
239.71/67.51	  , b(a(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.51	  , b(b(a(x1))) -> b(b(b(b(b(x1))))) }
239.71/67.51	Obligation:
239.71/67.51	  derivational complexity
239.71/67.51	Answer:
239.71/67.51	  YES(O(1),O(n^1))
239.71/67.51	
239.71/67.51	We use the processor 'matrix interpretation of dimension 3' to
239.71/67.51	orient following rules strictly.
239.71/67.51	
239.71/67.51	Trs: { a(a(a(x1))) -> a(a(b(a(a(x1))))) }
239.71/67.51	
239.71/67.51	The induced complexity on above rules (modulo remaining rules) is
239.71/67.51	YES(?,O(n^1)) . These rules are moved into the corresponding weak
239.71/67.51	component(s).
239.71/67.51	
239.71/67.51	Sub-proof:
239.71/67.51	----------
239.71/67.51	  TcT has computed the following triangular matrix interpretation.
239.71/67.51	  Note that the diagonal of the component-wise maxima of
239.71/67.51	  interpretation-entries contains no more than 1 non-zero entries.
239.71/67.51	  
239.71/67.51	              [1 1 0]      [0]
239.71/67.51	    [a](x1) = [0 0 1] x1 + [0]
239.71/67.51	              [0 0 0]      [1]
239.71/67.51	                              
239.71/67.51	              [1 0 0]      [0]
239.71/67.51	    [b](x1) = [0 0 0] x1 + [0]
239.71/67.51	              [0 0 0]      [0]
239.71/67.51	  
239.71/67.51	  The order satisfies the following ordering constraints:
239.71/67.51	  
239.71/67.51	          [a(x1)] =  [1 1 0]      [0]   
239.71/67.51	                     [0 0 1] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 0 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [0]   
239.71/67.51	                  =  [b(x1)]            
239.71/67.51	                                        
239.71/67.51	       [a(a(x1))] =  [1 1 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [1]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >= [1 1 0]      [0]   
239.71/67.51	                     [0 0 0] x1 + [0]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  =  [a(b(a(x1)))]      
239.71/67.51	                                        
239.71/67.51	    [a(a(a(x1)))] =  [1 1 1]      [1]   
239.71/67.51	                     [0 0 0] x1 + [1]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  >  [1 1 1]      [0]   
239.71/67.51	                     [0 0 0] x1 + [1]   
239.71/67.51	                     [0 0 0]      [1]   
239.71/67.51	                  =  [a(a(b(a(a(x1)))))]
239.71/67.51	                                        
239.71/67.51	    [a(a(b(x1)))] =  [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  =  [a(b(b(a(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	       [a(b(x1))] =  [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(x1)))]      
239.71/67.52	                                        
239.71/67.52	    [a(b(a(x1)))] =  [1 1 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  =  [a(b(b(a(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [a(b(a(x1)))] =  [1 1 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 1 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(a(b(b(a(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [a(b(b(x1)))] =  [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(b(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	       [b(a(x1))] =  [1 1 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(x1)))]      
239.71/67.52	                                        
239.71/67.52	    [b(a(a(x1)))] =  [1 1 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  >= [1 1 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(a(b(b(a(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [b(b(a(x1)))] =  [1 1 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(b(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	
239.71/67.52	We return to the main proof.
239.71/67.52	
239.71/67.52	We are left with following problem, upon which TcT provides the
239.71/67.52	certificate YES(O(1),O(n^1)).
239.71/67.52	
239.71/67.52	Strict Trs:
239.71/67.52	  { a(b(a(x1))) -> a(b(b(a(b(x1)))))
239.71/67.52	  , a(b(a(x1))) -> b(a(b(b(a(x1))))) }
239.71/67.52	Weak Trs:
239.71/67.52	  { a(x1) -> b(x1)
239.71/67.52	  , a(a(x1)) -> a(b(a(x1)))
239.71/67.52	  , a(a(a(x1))) -> a(a(b(a(a(x1)))))
239.71/67.52	  , a(a(b(x1))) -> a(b(b(a(b(x1)))))
239.71/67.52	  , a(b(x1)) -> b(b(b(x1)))
239.71/67.52	  , a(b(b(x1))) -> b(b(b(b(b(x1)))))
239.71/67.52	  , b(a(x1)) -> b(b(b(x1)))
239.71/67.52	  , b(a(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.52	  , b(b(a(x1))) -> b(b(b(b(b(x1))))) }
239.71/67.52	Obligation:
239.71/67.52	  derivational complexity
239.71/67.52	Answer:
239.71/67.52	  YES(O(1),O(n^1))
239.71/67.52	
239.71/67.52	We use the processor 'matrix interpretation of dimension 3' to
239.71/67.52	orient following rules strictly.
239.71/67.52	
239.71/67.52	Trs:
239.71/67.52	  { a(b(a(x1))) -> a(b(b(a(b(x1)))))
239.71/67.52	  , a(b(a(x1))) -> b(a(b(b(a(x1))))) }
239.71/67.52	
239.71/67.52	The induced complexity on above rules (modulo remaining rules) is
239.71/67.52	YES(?,O(n^1)) . These rules are moved into the corresponding weak
239.71/67.52	component(s).
239.71/67.52	
239.71/67.52	Sub-proof:
239.71/67.52	----------
239.71/67.52	  TcT has computed the following triangular matrix interpretation.
239.71/67.52	  Note that the diagonal of the component-wise maxima of
239.71/67.52	  interpretation-entries contains no more than 1 non-zero entries.
239.71/67.52	  
239.71/67.52	              [1 1 1]      [0]
239.71/67.52	    [a](x1) = [0 0 2] x1 + [1]
239.71/67.52	              [0 0 0]      [1]
239.71/67.52	                              
239.71/67.52	              [1 0 0]      [0]
239.71/67.52	    [b](x1) = [0 0 1] x1 + [0]
239.71/67.52	              [0 0 0]      [0]
239.71/67.52	  
239.71/67.52	  The order satisfies the following ordering constraints:
239.71/67.52	  
239.71/67.52	          [a(x1)] =  [1 1 1]      [0]   
239.71/67.52	                     [0 0 2] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 1] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(x1)]            
239.71/67.52	                                        
239.71/67.52	       [a(a(x1))] =  [1 1 3]      [2]   
239.71/67.52	                     [0 0 0] x1 + [3]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >  [1 1 1]      [1]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  =  [a(b(a(x1)))]      
239.71/67.52	                                        
239.71/67.52	    [a(a(a(x1)))] =  [1 1 3]      [6]   
239.71/67.52	                     [0 0 0] x1 + [3]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >  [1 1 3]      [5]   
239.71/67.52	                     [0 0 0] x1 + [3]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  =  [a(a(b(a(a(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [a(a(b(x1)))] =  [1 0 1]      [2]   
239.71/67.52	                     [0 0 0] x1 + [3]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >  [1 0 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  =  [a(b(b(a(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	       [a(b(x1))] =  [1 0 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(x1)))]      
239.71/67.52	                                        
239.71/67.52	    [a(b(a(x1)))] =  [1 1 1]      [1]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >  [1 0 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  =  [a(b(b(a(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [a(b(a(x1)))] =  [1 1 1]      [1]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >  [1 1 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(a(b(b(a(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [a(b(b(x1)))] =  [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [1]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(b(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	       [b(a(x1))] =  [1 1 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(x1)))]      
239.71/67.52	                                        
239.71/67.52	    [b(a(a(x1)))] =  [1 1 3]      [2]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  >  [1 1 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [1]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(a(b(b(a(x1)))))]
239.71/67.52	                                        
239.71/67.52	    [b(b(a(x1)))] =  [1 1 1]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  >= [1 0 0]      [0]   
239.71/67.52	                     [0 0 0] x1 + [0]   
239.71/67.52	                     [0 0 0]      [0]   
239.71/67.52	                  =  [b(b(b(b(b(x1)))))]
239.71/67.52	                                        
239.71/67.52	
239.71/67.52	We return to the main proof.
239.71/67.52	
239.71/67.52	We are left with following problem, upon which TcT provides the
239.71/67.52	certificate YES(O(1),O(1)).
239.71/67.52	
239.71/67.52	Weak Trs:
239.71/67.52	  { a(x1) -> b(x1)
239.71/67.52	  , a(a(x1)) -> a(b(a(x1)))
239.71/67.52	  , a(a(a(x1))) -> a(a(b(a(a(x1)))))
239.71/67.52	  , a(a(b(x1))) -> a(b(b(a(b(x1)))))
239.71/67.52	  , a(b(x1)) -> b(b(b(x1)))
239.71/67.52	  , a(b(a(x1))) -> a(b(b(a(b(x1)))))
239.71/67.52	  , a(b(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.52	  , a(b(b(x1))) -> b(b(b(b(b(x1)))))
239.71/67.52	  , b(a(x1)) -> b(b(b(x1)))
239.71/67.52	  , b(a(a(x1))) -> b(a(b(b(a(x1)))))
239.71/67.52	  , b(b(a(x1))) -> b(b(b(b(b(x1))))) }
239.71/67.52	Obligation:
239.71/67.52	  derivational complexity
239.71/67.52	Answer:
239.71/67.52	  YES(O(1),O(1))
239.71/67.52	
239.71/67.52	Empty rules are trivially bounded
239.71/67.52	
239.71/67.52	Hurray, we answered YES(O(1),O(n^1))
239.85/67.66	EOF