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