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