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