YES(?,O(n^1))
4.59/2.79	YES(?,O(n^1))
4.59/2.79	
4.59/2.79	We are left with following problem, upon which TcT provides the
4.59/2.79	certificate YES(?,O(n^1)).
4.59/2.79	
4.59/2.79	Strict Trs: { a(a(x)) -> a(b(a(x))) }
4.59/2.79	Obligation:
4.59/2.79	  derivational complexity
4.59/2.79	Answer:
4.59/2.79	  YES(?,O(n^1))
4.59/2.79	
4.59/2.79	TcT has computed the following matrix interpretation satisfying
4.59/2.79	not(EDA) and not(IDA(1)).
4.59/2.79	
4.59/2.79	            [1 0 0 1]      [0]
4.59/2.79	  [a](x1) = [0 0 0 0] x1 + [0]
4.59/2.79	            [0 0 0 0]      [0]
4.59/2.79	            [0 0 0 0]      [1]
4.59/2.79	                              
4.59/2.79	            [1 0 0 0]      [0]
4.59/2.79	  [b](x1) = [0 0 0 0] x1 + [0]
4.59/2.79	            [0 0 0 0]      [0]
4.59/2.79	            [0 0 0 0]      [0]
4.59/2.79	
4.59/2.79	The order satisfies the following ordering constraints:
4.59/2.79	
4.59/2.79	  [a(a(x))] = [1 0 0 1]     [1]
4.59/2.79	              [0 0 0 0] x + [0]
4.59/2.79	              [0 0 0 0]     [0]
4.59/2.79	              [0 0 0 0]     [1]
4.59/2.79	            > [1 0 0 1]     [0]
4.59/2.79	              [0 0 0 0] x + [0]
4.59/2.79	              [0 0 0 0]     [0]
4.59/2.79	              [0 0 0 0]     [1]
4.59/2.79	            = [a(b(a(x)))]     
4.59/2.79	                               
4.59/2.79	
4.59/2.79	Hurray, we answered YES(?,O(n^1))
4.74/2.80	EOF