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