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