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