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