YES(O(1),O(n^1))
185.77/60.02	YES(O(1),O(n^1))
185.77/60.02	
185.77/60.02	We are left with following problem, upon which TcT provides the
185.77/60.02	certificate YES(O(1),O(n^1)).
185.77/60.02	
185.77/60.02	Strict Trs:
185.77/60.02	  { f(x) -> g(x)
185.77/60.02	  , f(a()) -> f(b())
185.77/60.02	  , g(b()) -> g(a()) }
185.77/60.02	Obligation:
185.77/60.02	  derivational complexity
185.77/60.02	Answer:
185.77/60.02	  YES(O(1),O(n^1))
185.77/60.02	
185.77/60.02	The weightgap principle applies (using the following nonconstant
185.77/60.02	growth matrix-interpretation)
185.77/60.02	
185.77/60.02	TcT has computed the following triangular matrix interpretation.
185.77/60.02	Note that the diagonal of the component-wise maxima of
185.77/60.02	interpretation-entries contains no more than 1 non-zero entries.
185.77/60.02	
185.77/60.02	  [f](x1) = [1] x1 + [1]
185.77/60.02	                        
185.77/60.02	      [a] = [0]         
185.77/60.02	                        
185.77/60.02	      [b] = [0]         
185.77/60.02	                        
185.77/60.02	  [g](x1) = [1] x1 + [0]
185.77/60.02	
185.77/60.02	The order satisfies the following ordering constraints:
185.77/60.02	
185.77/60.02	    [f(x)] =  [1] x + [1]
185.77/60.02	           >  [1] x + [0]
185.77/60.02	           =  [g(x)]     
185.77/60.02	                         
185.77/60.02	  [f(a())] =  [1]        
185.77/60.02	           >= [1]        
185.77/60.02	           =  [f(b())]   
185.77/60.02	                         
185.77/60.02	  [g(b())] =  [0]        
185.77/60.02	           >= [0]        
185.77/60.02	           =  [g(a())]   
185.77/60.02	                         
185.77/60.02	
185.77/60.02	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
185.77/60.02	
185.77/60.02	We are left with following problem, upon which TcT provides the
185.77/60.02	certificate YES(O(1),O(n^1)).
185.77/60.02	
185.77/60.02	Strict Trs:
185.77/60.02	  { f(a()) -> f(b())
185.77/60.02	  , g(b()) -> g(a()) }
185.77/60.02	Weak Trs: { f(x) -> g(x) }
185.77/60.02	Obligation:
185.77/60.02	  derivational complexity
185.77/60.02	Answer:
185.77/60.02	  YES(O(1),O(n^1))
185.77/60.02	
185.77/60.02	The weightgap principle applies (using the following nonconstant
185.77/60.02	growth matrix-interpretation)
185.77/60.02	
185.77/60.02	TcT has computed the following triangular matrix interpretation.
185.77/60.02	Note that the diagonal of the component-wise maxima of
185.77/60.02	interpretation-entries contains no more than 1 non-zero entries.
185.77/60.02	
185.77/60.02	  [f](x1) = [1] x1 + [0]
185.77/60.02	                        
185.77/60.02	      [a] = [0]         
185.77/60.02	                        
185.77/60.02	      [b] = [1]         
185.77/60.02	                        
185.77/60.02	  [g](x1) = [1] x1 + [0]
185.77/60.02	
185.77/60.02	The order satisfies the following ordering constraints:
185.77/60.02	
185.77/60.02	    [f(x)] =  [1] x + [0]
185.77/60.02	           >= [1] x + [0]
185.77/60.02	           =  [g(x)]     
185.77/60.02	                         
185.77/60.02	  [f(a())] =  [0]        
185.77/60.02	           ?  [1]        
185.77/60.02	           =  [f(b())]   
185.77/60.02	                         
185.77/60.02	  [g(b())] =  [1]        
185.77/60.02	           >  [0]        
185.77/60.02	           =  [g(a())]   
185.77/60.02	                         
185.77/60.02	
185.77/60.02	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
185.77/60.02	
185.77/60.02	We are left with following problem, upon which TcT provides the
185.77/60.02	certificate YES(O(1),O(n^1)).
185.77/60.02	
185.77/60.02	Strict Trs: { f(a()) -> f(b()) }
185.77/60.02	Weak Trs:
185.77/60.02	  { f(x) -> g(x)
185.77/60.02	  , g(b()) -> g(a()) }
185.77/60.02	Obligation:
185.77/60.02	  derivational complexity
185.77/60.02	Answer:
185.77/60.02	  YES(O(1),O(n^1))
185.77/60.02	
185.77/60.02	We use the processor 'matrix interpretation of dimension 2' to
185.77/60.02	orient following rules strictly.
185.77/60.02	
185.77/60.02	Trs: { f(a()) -> f(b()) }
185.77/60.02	
185.77/60.02	The induced complexity on above rules (modulo remaining rules) is
185.77/60.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
185.77/60.02	component(s).
185.77/60.02	
185.77/60.02	Sub-proof:
185.77/60.02	----------
185.77/60.02	  TcT has computed the following triangular matrix interpretation.
185.77/60.02	  Note that the diagonal of the component-wise maxima of
185.77/60.02	  interpretation-entries contains no more than 1 non-zero entries.
185.77/60.02	  
185.77/60.02	    [f](x1) = [1 2] x1 + [0]
185.77/60.02	              [0 0]      [2]
185.77/60.02	                            
185.77/60.02	        [a] = [0]           
185.77/60.02	              [2]           
185.77/60.02	                            
185.77/60.02	        [b] = [0]           
185.77/60.02	              [0]           
185.77/60.02	                            
185.77/60.02	    [g](x1) = [1 0] x1 + [0]
185.77/60.02	              [0 0]      [2]
185.77/60.02	  
185.77/60.02	  The order satisfies the following ordering constraints:
185.77/60.02	  
185.77/60.02	      [f(x)] =  [1 2] x + [0]
185.77/60.02	                [0 0]     [2]
185.77/60.02	             >= [1 0] x + [0]
185.77/60.02	                [0 0]     [2]
185.77/60.02	             =  [g(x)]       
185.77/60.02	                             
185.77/60.02	    [f(a())] =  [4]          
185.77/60.02	                [2]          
185.77/60.02	             >  [0]          
185.77/60.02	                [2]          
185.77/60.02	             =  [f(b())]     
185.77/60.02	                             
185.77/60.02	    [g(b())] =  [0]          
185.77/60.02	                [2]          
185.77/60.02	             >= [0]          
185.77/60.02	                [2]          
185.77/60.02	             =  [g(a())]     
185.77/60.02	                             
185.77/60.02	
185.77/60.02	We return to the main proof.
185.77/60.02	
185.77/60.02	We are left with following problem, upon which TcT provides the
185.77/60.02	certificate YES(O(1),O(1)).
185.77/60.02	
185.77/60.02	Weak Trs:
185.77/60.02	  { f(x) -> g(x)
185.77/60.02	  , f(a()) -> f(b())
185.77/60.02	  , g(b()) -> g(a()) }
185.77/60.02	Obligation:
185.77/60.02	  derivational complexity
185.77/60.02	Answer:
185.77/60.02	  YES(O(1),O(1))
185.77/60.02	
185.77/60.02	Empty rules are trivially bounded
185.77/60.02	
185.77/60.02	Hurray, we answered YES(O(1),O(n^1))
185.77/60.03	EOF