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