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