YES(O(1),O(n^3))
157.36/60.02	YES(O(1),O(n^3))
157.36/60.02	
157.36/60.02	We are left with following problem, upon which TcT provides the
157.36/60.02	certificate YES(O(1),O(n^3)).
157.36/60.02	
157.36/60.02	Strict Trs:
157.36/60.02	  { a(x1) -> b(c(x1))
157.36/60.02	  , a(b(x1)) -> b(a(x1))
157.36/60.02	  , a(c(x1)) -> c(a(x1))
157.36/60.02	  , d(c(x1)) -> d(a(x1)) }
157.36/60.02	Obligation:
157.36/60.02	  derivational complexity
157.36/60.02	Answer:
157.36/60.02	  YES(O(1),O(n^3))
157.36/60.02	
157.36/60.02	We use the processor 'matrix interpretation of dimension 2' to
157.36/60.02	orient following rules strictly.
157.36/60.02	
157.36/60.02	Trs:
157.36/60.02	  { a(x1) -> b(c(x1))
157.36/60.02	  , d(c(x1)) -> d(a(x1)) }
157.36/60.02	
157.36/60.02	The induced complexity on above rules (modulo remaining rules) is
157.36/60.02	YES(?,O(n^1)) . These rules are removed from the problem. Note that
157.36/60.02	none of the weakly oriented rules is size-increasing. The overall
157.36/60.02	complexity is obtained by composition .
157.36/60.02	
157.36/60.02	Sub-proof:
157.36/60.02	----------
157.36/60.02	  TcT has computed the following triangular matrix interpretation.
157.36/60.02	  
157.36/60.02	    [a](x1) = [1 0] x1 + [1]
157.36/60.02	              [0 1]      [0]
157.36/60.02	                            
157.36/60.02	    [b](x1) = [1 0] x1 + [0]
157.36/60.02	              [0 0]      [0]
157.36/60.02	                            
157.36/60.02	    [c](x1) = [1 0] x1 + [0]
157.36/60.02	              [0 1]      [1]
157.36/60.02	                            
157.36/60.02	    [d](x1) = [1 2] x1 + [0]
157.36/60.02	              [0 0]      [0]
157.36/60.02	  
157.36/60.02	  The order satisfies the following ordering constraints:
157.36/60.02	  
157.36/60.02	       [a(x1)] =  [1 0] x1 + [1]
157.36/60.02	                  [0 1]      [0]
157.36/60.02	               >  [1 0] x1 + [0]
157.36/60.02	                  [0 0]      [0]
157.36/60.02	               =  [b(c(x1))]    
157.36/60.02	                                
157.36/60.02	    [a(b(x1))] =  [1 0] x1 + [1]
157.36/60.02	                  [0 0]      [0]
157.36/60.02	               >= [1 0] x1 + [1]
157.36/60.02	                  [0 0]      [0]
157.36/60.02	               =  [b(a(x1))]    
157.36/60.02	                                
157.36/60.02	    [a(c(x1))] =  [1 0] x1 + [1]
157.36/60.02	                  [0 1]      [1]
157.36/60.02	               >= [1 0] x1 + [1]
157.36/60.02	                  [0 1]      [1]
157.36/60.02	               =  [c(a(x1))]    
157.36/60.02	                                
157.36/60.02	    [d(c(x1))] =  [1 2] x1 + [2]
157.36/60.02	                  [0 0]      [0]
157.36/60.02	               >  [1 2] x1 + [1]
157.36/60.02	                  [0 0]      [0]
157.36/60.02	               =  [d(a(x1))]    
157.36/60.02	                                
157.36/60.02	
157.36/60.02	We return to the main proof.
157.36/60.02	
157.36/60.02	We are left with following problem, upon which TcT provides the
157.36/60.02	certificate YES(?,O(n^2)).
157.36/60.02	
157.36/60.02	Strict Trs:
157.36/60.02	  { a(b(x1)) -> b(a(x1))
157.36/60.02	  , a(c(x1)) -> c(a(x1)) }
157.36/60.02	Obligation:
157.36/60.02	  derivational complexity
157.36/60.02	Answer:
157.36/60.02	  YES(?,O(n^2))
157.36/60.02	
157.36/60.02	TcT has computed the following triangular matrix interpretation.
157.36/60.02	
157.36/60.02	  [a](x1) = [1 1] x1 + [0]
157.36/60.02	            [0 1]      [4]
157.36/60.02	                          
157.36/60.02	  [b](x1) = [1 0] x1 + [0]
157.36/60.02	            [0 1]      [4]
157.36/60.02	                          
157.36/60.02	  [c](x1) = [1 0] x1 + [0]
157.36/60.02	            [0 1]      [4]
157.36/60.02	
157.36/60.02	The order satisfies the following ordering constraints:
157.36/60.02	
157.36/60.02	  [a(b(x1))] = [1 1] x1 + [4]
157.36/60.02	               [0 1]      [8]
157.36/60.02	             > [1 1] x1 + [0]
157.36/60.02	               [0 1]      [8]
157.36/60.02	             = [b(a(x1))]    
157.36/60.02	                             
157.36/60.02	  [a(c(x1))] = [1 1] x1 + [4]
157.36/60.02	               [0 1]      [8]
157.36/60.02	             > [1 1] x1 + [0]
157.36/60.02	               [0 1]      [8]
157.36/60.02	             = [c(a(x1))]    
157.36/60.02	                             
157.36/60.02	
157.36/60.02	Hurray, we answered YES(O(1),O(n^3))
157.36/60.05	EOF