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