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