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