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