YES(O(1),O(n^1))
187.05/60.08	YES(O(1),O(n^1))
187.05/60.08	
187.05/60.08	We are left with following problem, upon which TcT provides the
187.05/60.08	certificate YES(O(1),O(n^1)).
187.05/60.08	
187.05/60.08	Strict Trs:
187.05/60.08	  { app(app(app(compose(), f), g), x) -> app(f, app(g, x)) }
187.05/60.08	Obligation:
187.05/60.08	  derivational complexity
187.05/60.08	Answer:
187.05/60.08	  YES(O(1),O(n^1))
187.05/60.08	
187.05/60.08	We uncurry the input using the following uncurry rules.
187.05/60.08	
187.05/60.08	  { app(compose(), x_1) -> compose_1(x_1)
187.05/60.08	  , app(compose_1(x_1), x_2) -> compose_2(x_1, x_2)
187.05/60.08	  , app(compose_2(x_1, x_2), x_3) -> compose_3(x_1, x_2, x_3) }
187.05/60.08	
187.05/60.08	We are left with following problem, upon which TcT provides the
187.05/60.08	certificate YES(O(1),O(n^1)).
187.05/60.08	
187.05/60.08	Strict Trs: { compose_3(f, g, x) -> app(f, app(g, x)) }
187.05/60.08	Weak Trs:
187.05/60.08	  { app(compose(), x_1) -> compose_1(x_1)
187.05/60.08	  , app(compose_1(x_1), x_2) -> compose_2(x_1, x_2)
187.05/60.08	  , app(compose_2(x_1, x_2), x_3) -> compose_3(x_1, x_2, x_3) }
187.05/60.08	Obligation:
187.05/60.08	  derivational complexity
187.05/60.08	Answer:
187.05/60.08	  YES(O(1),O(n^1))
187.05/60.08	
187.05/60.08	We use the processor 'matrix interpretation of dimension 1' to
187.05/60.08	orient following rules strictly.
187.05/60.08	
187.05/60.08	Trs: { compose_3(f, g, x) -> app(f, app(g, x)) }
187.05/60.08	
187.05/60.08	The induced complexity on above rules (modulo remaining rules) is
187.05/60.08	YES(?,O(n^1)) . These rules are moved into the corresponding weak
187.05/60.08	component(s).
187.05/60.08	
187.05/60.08	Sub-proof:
187.05/60.08	----------
187.05/60.08	  TcT has computed the following triangular matrix interpretation.
187.05/60.08	  
187.05/60.08	              [app](x1, x2) = [1] x1 + [1] x2 + [0]         
187.05/60.08	                                                            
187.05/60.08	    [compose_3](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1]
187.05/60.08	                                                            
187.05/60.08	                  [compose] = [2]                           
187.05/60.08	                                                            
187.05/60.08	            [compose_1](x1) = [1] x1 + [2]                  
187.05/60.08	                                                            
187.05/60.08	        [compose_2](x1, x2) = [1] x1 + [1] x2 + [1]         
187.05/60.08	  
187.05/60.08	  The order satisfies the following ordering constraints:
187.05/60.08	  
187.05/60.08	              [app(compose(), x_1)] =  [1] x_1 + [2]                    
187.05/60.08	                                    >= [1] x_1 + [2]                    
187.05/60.08	                                    =  [compose_1(x_1)]                 
187.05/60.08	                                                                        
187.05/60.08	         [app(compose_1(x_1), x_2)] =  [1] x_1 + [1] x_2 + [2]          
187.05/60.08	                                    >  [1] x_1 + [1] x_2 + [1]          
187.05/60.08	                                    =  [compose_2(x_1, x_2)]            
187.05/60.08	                                                                        
187.05/60.08	    [app(compose_2(x_1, x_2), x_3)] =  [1] x_1 + [1] x_2 + [1] x_3 + [1]
187.05/60.08	                                    >= [1] x_1 + [1] x_2 + [1] x_3 + [1]
187.05/60.08	                                    =  [compose_3(x_1, x_2, x_3)]       
187.05/60.08	                                                                        
187.05/60.08	               [compose_3(f, g, x)] =  [1] f + [1] g + [1] x + [1]      
187.05/60.08	                                    >  [1] f + [1] g + [1] x + [0]      
187.05/60.08	                                    =  [app(f, app(g, x))]              
187.05/60.08	                                                                        
187.05/60.08	
187.05/60.08	We return to the main proof.
187.05/60.08	
187.05/60.08	We are left with following problem, upon which TcT provides the
187.05/60.08	certificate YES(O(1),O(1)).
187.05/60.08	
187.05/60.08	Weak Trs:
187.05/60.08	  { app(compose(), x_1) -> compose_1(x_1)
187.05/60.08	  , app(compose_1(x_1), x_2) -> compose_2(x_1, x_2)
187.05/60.08	  , app(compose_2(x_1, x_2), x_3) -> compose_3(x_1, x_2, x_3)
187.05/60.08	  , compose_3(f, g, x) -> app(f, app(g, x)) }
187.05/60.08	Obligation:
187.05/60.08	  derivational complexity
187.05/60.08	Answer:
187.05/60.08	  YES(O(1),O(1))
187.05/60.08	
187.05/60.08	Empty rules are trivially bounded
187.05/60.08	
187.05/60.08	Hurray, we answered YES(O(1),O(n^1))
187.05/60.08	EOF