YES(O(1),O(n^1))
143.16/60.02	YES(O(1),O(n^1))
143.16/60.02	
143.16/60.02	We are left with following problem, upon which TcT provides the
143.16/60.02	certificate YES(O(1),O(n^1)).
143.16/60.02	
143.16/60.02	Strict Trs:
143.16/60.02	  { f(x, x, y) -> x
143.16/60.02	  , f(x, y, y) -> y
143.16/60.02	  , f(x, y, g(y)) -> x
143.16/60.02	  , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))
143.16/60.02	  , f(g(x), x, y) -> y }
143.16/60.02	Obligation:
143.16/60.02	  derivational complexity
143.16/60.02	Answer:
143.16/60.02	  YES(O(1),O(n^1))
143.16/60.02	
143.16/60.02	We use the processor 'matrix interpretation of dimension 1' to
143.16/60.02	orient following rules strictly.
143.16/60.02	
143.16/60.02	Trs:
143.16/60.02	  { f(x, y, g(y)) -> x
143.16/60.02	  , f(g(x), x, y) -> y }
143.16/60.02	
143.16/60.02	The induced complexity on above rules (modulo remaining rules) is
143.16/60.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
143.16/60.02	component(s).
143.16/60.02	
143.16/60.02	Sub-proof:
143.16/60.02	----------
143.16/60.02	  TcT has computed the following triangular matrix interpretation.
143.16/60.02	  
143.16/60.02	    [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [0]
143.16/60.02	                                                    
143.16/60.02	            [g](x1) = [1] x1 + [2]                  
143.16/60.02	  
143.16/60.02	  The order satisfies the following ordering constraints:
143.16/60.02	  
143.16/60.02	                      [f(x, x, y)] =  [2] x + [1] y + [0]                        
143.16/60.02	                                   >= [1] x + [0]                                
143.16/60.02	                                   =  [x]                                        
143.16/60.02	                                                                                 
143.16/60.02	                      [f(x, y, y)] =  [1] x + [2] y + [0]                        
143.16/60.02	                                   >= [1] y + [0]                                
143.16/60.02	                                   =  [y]                                        
143.16/60.02	                                                                                 
143.16/60.02	                   [f(x, y, g(y))] =  [1] x + [2] y + [2]                        
143.16/60.02	                                   >  [1] x + [0]                                
143.16/60.02	                                   =  [x]                                        
143.16/60.02	                                                                                 
143.16/60.02	    [f(f(x, y, z), u, f(x, y, v))] =  [2] x + [2] y + [1] z + [1] u + [1] v + [0]
143.16/60.02	                                   >= [1] x + [1] y + [1] z + [1] u + [1] v + [0]
143.16/60.02	                                   =  [f(x, y, f(z, u, v))]                      
143.16/60.02	                                                                                 
143.16/60.02	                   [f(g(x), x, y)] =  [2] x + [1] y + [2]                        
143.16/60.02	                                   >  [1] y + [0]                                
143.16/60.02	                                   =  [y]                                        
143.16/60.02	                                                                                 
143.16/60.02	
143.16/60.02	We return to the main proof.
143.16/60.02	
143.16/60.02	We are left with following problem, upon which TcT provides the
143.16/60.02	certificate YES(O(1),O(n^1)).
143.16/60.02	
143.16/60.02	Strict Trs:
143.16/60.02	  { f(x, x, y) -> x
143.16/60.02	  , f(x, y, y) -> y
143.16/60.02	  , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) }
143.16/60.02	Weak Trs:
143.16/60.02	  { f(x, y, g(y)) -> x
143.16/60.02	  , f(g(x), x, y) -> y }
143.16/60.02	Obligation:
143.16/60.02	  derivational complexity
143.16/60.02	Answer:
143.16/60.02	  YES(O(1),O(n^1))
143.16/60.02	
143.16/60.02	We use the processor 'matrix interpretation of dimension 1' to
143.16/60.02	orient following rules strictly.
143.16/60.02	
143.16/60.02	Trs:
143.16/60.02	  { f(x, x, y) -> x
143.16/60.02	  , f(x, y, y) -> y
143.16/60.02	  , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) }
143.16/60.02	
143.16/60.02	The induced complexity on above rules (modulo remaining rules) is
143.16/60.02	YES(?,O(n^1)) . These rules are moved into the corresponding weak
143.16/60.02	component(s).
143.16/60.02	
143.16/60.02	Sub-proof:
143.16/60.02	----------
143.16/60.02	  TcT has computed the following triangular matrix interpretation.
143.16/60.02	  
143.16/60.02	    [f](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [2]
143.16/60.02	                                                    
143.16/60.02	            [g](x1) = [1] x1 + [1]                  
143.16/60.02	  
143.16/60.02	  The order satisfies the following ordering constraints:
143.16/60.02	  
143.16/60.02	                      [f(x, x, y)] = [2] x + [1] y + [2]                        
143.16/60.02	                                   > [1] x + [0]                                
143.16/60.02	                                   = [x]                                        
143.16/60.02	                                                                                
143.16/60.02	                      [f(x, y, y)] = [1] x + [2] y + [2]                        
143.16/60.02	                                   > [1] y + [0]                                
143.16/60.02	                                   = [y]                                        
143.16/60.02	                                                                                
143.16/60.02	                   [f(x, y, g(y))] = [1] x + [2] y + [3]                        
143.16/60.02	                                   > [1] x + [0]                                
143.16/60.02	                                   = [x]                                        
143.16/60.02	                                                                                
143.16/60.02	    [f(f(x, y, z), u, f(x, y, v))] = [2] x + [2] y + [1] z + [1] u + [1] v + [6]
143.16/60.02	                                   > [1] x + [1] y + [1] z + [1] u + [1] v + [4]
143.16/60.02	                                   = [f(x, y, f(z, u, v))]                      
143.16/60.02	                                                                                
143.16/60.02	                   [f(g(x), x, y)] = [2] x + [1] y + [3]                        
143.16/60.02	                                   > [1] y + [0]                                
143.16/60.02	                                   = [y]                                        
143.16/60.02	                                                                                
143.16/60.02	
143.16/60.02	We return to the main proof.
143.16/60.02	
143.16/60.02	We are left with following problem, upon which TcT provides the
143.16/60.02	certificate YES(O(1),O(1)).
143.16/60.02	
143.16/60.02	Weak Trs:
143.16/60.02	  { f(x, x, y) -> x
143.16/60.02	  , f(x, y, y) -> y
143.16/60.02	  , f(x, y, g(y)) -> x
143.16/60.02	  , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v))
143.16/60.02	  , f(g(x), x, y) -> y }
143.16/60.02	Obligation:
143.16/60.02	  derivational complexity
143.16/60.02	Answer:
143.16/60.02	  YES(O(1),O(1))
143.16/60.02	
143.16/60.02	Empty rules are trivially bounded
143.16/60.02	
143.16/60.02	Hurray, we answered YES(O(1),O(n^1))
143.16/60.06	EOF