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