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