YES(?,O(n^1))
8.09/4.63	YES(?,O(n^1))
8.09/4.63	
8.09/4.63	We are left with following problem, upon which TcT provides the
8.09/4.63	certificate YES(?,O(n^1)).
8.09/4.63	
8.09/4.63	Strict Trs:
8.09/4.63	  { f(a(), f(a(), x)) -> f(a(), f(f(a(), x), f(a(), a()))) }
8.09/4.63	Obligation:
8.09/4.63	  derivational complexity
8.09/4.63	Answer:
8.09/4.63	  YES(?,O(n^1))
8.09/4.63	
8.09/4.63	We uncurry the input using the following uncurry rules.
8.09/4.63	
8.09/4.63	  { f(a_1(x_1), x_2) -> a_2(x_1, x_2)
8.09/4.63	  , f(a(), x_1) -> a_1(x_1) }
8.09/4.63	
8.09/4.63	We are left with following problem, upon which TcT provides the
8.09/4.63	certificate YES(?,O(n^1)).
8.09/4.63	
8.09/4.63	Strict Trs: { a_2(a_1(x), x_1) -> a_2(a_2(x, a_1(a())), x_1) }
8.09/4.63	Weak Trs:
8.09/4.63	  { f(a_1(x_1), x_2) -> a_2(x_1, x_2)
8.09/4.63	  , f(a(), x_1) -> a_1(x_1) }
8.09/4.63	Obligation:
8.09/4.63	  derivational complexity
8.09/4.63	Answer:
8.09/4.63	  YES(?,O(n^1))
8.09/4.63	
8.09/4.63	TcT has computed the following matrix interpretation satisfying
8.09/4.63	not(EDA) and not(IDA(1)).
8.09/4.63	
8.09/4.63	                  [1 0 0 0]      [1 0 1 0]      [1]
8.09/4.63	    [f](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
8.09/4.63	                  [0 0 0 0]      [0 0 0 0]      [1]
8.09/4.63	                  [0 0 0 0]      [0 0 0 0]      [1]
8.09/4.63	                                                   
8.09/4.63	                  [1 0 1 0]      [1 0 0 0]      [0]
8.09/4.63	  [a_2](x1, x2) = [0 0 0 0] x1 + [0 0 0 0] x2 + [0]
8.09/4.63	                  [0 0 0 0]      [0 0 0 0]      [0]
8.09/4.63	                  [0 0 0 0]      [0 0 0 0]      [0]
8.09/4.63	                                                   
8.09/4.63	                  [1 0 1 0]      [0]               
8.09/4.63	      [a_1](x1) = [0 0 0 0] x1 + [0]               
8.09/4.63	                  [0 0 0 0]      [1]               
8.09/4.63	                  [0 0 0 0]      [0]               
8.09/4.63	                                                   
8.09/4.63	                  [0]                              
8.09/4.63	            [a] = [0]                              
8.09/4.63	                  [0]                              
8.09/4.63	                  [0]                              
8.09/4.63	
8.09/4.63	The order satisfies the following ordering constraints:
8.09/4.63	
8.09/4.63	  [f(a_1(x_1), x_2)] = [1 0 1 0]       [1 0 1 0]       [1]
8.09/4.63	                       [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0]
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]       [1]
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]       [1]
8.09/4.63	                     > [1 0 1 0]       [1 0 0 0]       [0]
8.09/4.63	                       [0 0 0 0] x_1 + [0 0 0 0] x_2 + [0]
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]       [0]
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]       [0]
8.09/4.63	                     = [a_2(x_1, x_2)]                    
8.09/4.63	                                                          
8.09/4.63	       [f(a(), x_1)] = [1 0 1 0]       [1]                
8.09/4.63	                       [0 0 0 0] x_1 + [0]                
8.09/4.63	                       [0 0 0 0]       [1]                
8.09/4.63	                       [0 0 0 0]       [1]                
8.09/4.63	                     > [1 0 1 0]       [0]                
8.09/4.63	                       [0 0 0 0] x_1 + [0]                
8.09/4.63	                       [0 0 0 0]       [1]                
8.09/4.63	                       [0 0 0 0]       [0]                
8.09/4.63	                     = [a_1(x_1)]                         
8.09/4.63	                                                          
8.09/4.63	  [a_2(a_1(x), x_1)] = [1 0 0 0]       [1 0 1 0]     [1]  
8.09/4.63	                       [0 0 0 0] x_1 + [0 0 0 0] x + [0]  
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]     [0]  
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]     [0]  
8.09/4.63	                     > [1 0 0 0]       [1 0 1 0]     [0]  
8.09/4.63	                       [0 0 0 0] x_1 + [0 0 0 0] x + [0]  
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]     [0]  
8.09/4.63	                       [0 0 0 0]       [0 0 0 0]     [0]  
8.09/4.63	                     = [a_2(a_2(x, a_1(a())), x_1)]       
8.09/4.63	                                                          
8.09/4.63	
8.09/4.63	Hurray, we answered YES(?,O(n^1))
8.09/4.65	EOF