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