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