YES(O(1),O(n^2))
173.37/60.07	YES(O(1),O(n^2))
173.37/60.07	
173.37/60.07	We are left with following problem, upon which TcT provides the
173.37/60.07	certificate YES(O(1),O(n^2)).
173.37/60.07	
173.37/60.07	Strict Trs:
173.37/60.07	  { a(a(x1)) -> a(b(a(x1)))
173.37/60.07	  , b(a(b(x1))) -> a(c(a(x1))) }
173.37/60.07	Obligation:
173.37/60.07	  derivational complexity
173.37/60.07	Answer:
173.37/60.07	  YES(O(1),O(n^2))
173.37/60.07	
173.37/60.07	The weightgap principle applies (using the following nonconstant
173.37/60.07	growth matrix-interpretation)
173.37/60.07	
173.37/60.07	TcT has computed the following triangular matrix interpretation.
173.37/60.07	Note that the diagonal of the component-wise maxima of
173.37/60.07	interpretation-entries contains no more than 1 non-zero entries.
173.37/60.07	
173.37/60.07	  [a](x1) = [1] x1 + [0]
173.37/60.07	                        
173.37/60.07	  [b](x1) = [1] x1 + [1]
173.37/60.07	                        
173.37/60.07	  [c](x1) = [1] x1 + [1]
173.37/60.07	
173.37/60.07	The order satisfies the following ordering constraints:
173.37/60.07	
173.37/60.07	     [a(a(x1))] = [1] x1 + [0] 
173.37/60.07	                ? [1] x1 + [1] 
173.37/60.07	                = [a(b(a(x1)))]
173.37/60.07	                               
173.37/60.07	  [b(a(b(x1)))] = [1] x1 + [2] 
173.37/60.07	                > [1] x1 + [1] 
173.37/60.07	                = [a(c(a(x1)))]
173.37/60.07	                               
173.37/60.07	
173.37/60.07	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
173.37/60.07	
173.37/60.07	We are left with following problem, upon which TcT provides the
173.37/60.07	certificate YES(?,O(n^2)).
173.37/60.07	
173.37/60.07	Strict Trs: { a(a(x1)) -> a(b(a(x1))) }
173.37/60.07	Weak Trs: { b(a(b(x1))) -> a(c(a(x1))) }
173.37/60.07	Obligation:
173.37/60.07	  derivational complexity
173.37/60.07	Answer:
173.37/60.07	  YES(?,O(n^2))
173.37/60.07	
173.37/60.07	TcT has computed the following triangular matrix interpretation.
173.37/60.07	
173.37/60.07	            [1 4 0 1 2]      [0]
173.37/60.07	            [0 0 2 1 0]      [0]
173.37/60.07	  [a](x1) = [0 0 0 0 1] x1 + [4]
173.37/60.07	            [0 0 0 0 0]      [4]
173.37/60.07	            [0 0 0 0 1]      [2]
173.37/60.07	                                
173.37/60.07	            [1 4 0 0 0]      [0]
173.37/60.07	            [0 0 0 0 0]      [0]
173.37/60.07	  [b](x1) = [0 0 0 1 0] x1 + [0]
173.37/60.07	            [0 0 0 0 1]      [1]
173.37/60.07	            [0 0 0 0 0]      [2]
173.37/60.07	                                
173.37/60.07	            [1 0 0 0 2]      [0]
173.37/60.07	            [0 0 0 0 0]      [0]
173.37/60.07	  [c](x1) = [0 0 0 0 0] x1 + [0]
173.37/60.07	            [0 0 0 0 0]      [0]
173.37/60.07	            [0 0 0 0 0]      [0]
173.37/60.07	
173.37/60.07	The order satisfies the following ordering constraints:
173.37/60.07	
173.37/60.07	     [a(a(x1))] = [1 4 8 5 4]      [8] 
173.37/60.07	                  [0 0 0 0 2]      [12]
173.37/60.07	                  [0 0 0 0 1] x1 + [6] 
173.37/60.07	                  [0 0 0 0 0]      [4] 
173.37/60.07	                  [0 0 0 0 1]      [4] 
173.37/60.07	                > [1 4 8 5 3]      [7] 
173.37/60.07	                  [0 0 0 0 1]      [11]
173.37/60.07	                  [0 0 0 0 0] x1 + [6] 
173.37/60.07	                  [0 0 0 0 0]      [4] 
173.37/60.07	                  [0 0 0 0 0]      [4] 
173.37/60.07	                = [a(b(a(x1)))]        
173.37/60.07	                                       
173.37/60.07	  [b(a(b(x1)))] = [1 4 0 8 5]      [9] 
173.37/60.07	                  [0 0 0 0 0]      [0] 
173.37/60.07	                  [0 0 0 0 0] x1 + [4] 
173.37/60.07	                  [0 0 0 0 0]      [5] 
173.37/60.07	                  [0 0 0 0 0]      [2] 
173.37/60.07	                > [1 4 0 1 4]      [4] 
173.37/60.07	                  [0 0 0 0 0]      [0] 
173.37/60.07	                  [0 0 0 0 0] x1 + [4] 
173.37/60.07	                  [0 0 0 0 0]      [4] 
173.37/60.07	                  [0 0 0 0 0]      [2] 
173.37/60.07	                = [a(c(a(x1)))]        
173.37/60.07	                                       
173.37/60.07	
173.37/60.07	Hurray, we answered YES(O(1),O(n^2))
173.37/60.09	EOF