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