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