YES(O(1),O(n^3))
338.56/164.47	YES(O(1),O(n^3))
338.56/164.47	
338.56/164.47	We are left with following problem, upon which TcT provides the
338.56/164.47	certificate YES(O(1),O(n^3)).
338.56/164.47	
338.56/164.47	Strict Trs:
338.56/164.47	  { +(+(x, y), z) -> +(x, +(y, z))
338.56/164.47	  , +(f(x), +(f(y), z)) -> +(f(+(x, y)), z)
338.56/164.47	  , +(f(x), f(y)) -> f(+(x, y)) }
338.56/164.47	Obligation:
338.56/164.47	  derivational complexity
338.56/164.47	Answer:
338.56/164.47	  YES(O(1),O(n^3))
338.56/164.47	
338.56/164.47	We use the processor 'matrix interpretation of dimension 1' to
338.56/164.47	orient following rules strictly.
338.56/164.47	
338.56/164.47	Trs:
338.56/164.47	  { +(f(x), +(f(y), z)) -> +(f(+(x, y)), z)
338.56/164.47	  , +(f(x), f(y)) -> f(+(x, y)) }
338.56/164.47	
338.56/164.47	The induced complexity on above rules (modulo remaining rules) is
338.56/164.47	YES(?,O(n^1)) . These rules are removed from the problem. Note that
338.56/164.47	no rule is size-increasing. The overall complexity is obtained by
338.56/164.47	multiplication .
338.56/164.47	
338.56/164.47	Sub-proof:
338.56/164.47	----------
338.56/164.47	  TcT has computed the following triangular matrix interpretation.
338.56/164.47	  
338.56/164.47	    [+](x1, x2) = [1] x1 + [1] x2 + [0]
338.56/164.47	                                       
338.56/164.47	        [f](x1) = [1] x1 + [2]         
338.56/164.47	  
338.56/164.47	  The order satisfies the following ordering constraints:
338.56/164.47	  
338.56/164.47	          [+(+(x, y), z)] =  [1] x + [1] y + [1] z + [0]
338.56/164.47	                          >= [1] x + [1] y + [1] z + [0]
338.56/164.47	                          =  [+(x, +(y, z))]            
338.56/164.47	                                                        
338.56/164.47	    [+(f(x), +(f(y), z))] =  [1] x + [1] y + [1] z + [4]
338.56/164.47	                          >  [1] x + [1] y + [1] z + [2]
338.56/164.47	                          =  [+(f(+(x, y)), z)]         
338.56/164.47	                                                        
338.56/164.47	          [+(f(x), f(y))] =  [1] x + [1] y + [4]        
338.56/164.47	                          >  [1] x + [1] y + [2]        
338.56/164.47	                          =  [f(+(x, y))]               
338.56/164.47	                                                        
338.56/164.47	
338.56/164.47	We return to the main proof.
338.56/164.47	
338.56/164.47	We are left with following problem, upon which TcT provides the
338.56/164.47	certificate YES(O(1),O(n^2)).
338.56/164.47	
338.56/164.47	Strict Trs: { +(+(x, y), z) -> +(x, +(y, z)) }
338.56/164.47	Obligation:
338.56/164.47	  derivational complexity
338.56/164.47	Answer:
338.56/164.47	  YES(O(1),O(n^2))
338.56/164.47	
338.56/164.47	We use the processor 'matrix interpretation of dimension 2' to
338.56/164.47	orient following rules strictly.
338.56/164.47	
338.56/164.47	Trs: { +(+(x, y), z) -> +(x, +(y, z)) }
338.56/164.47	
338.56/164.47	The induced complexity on above rules (modulo remaining rules) is
338.56/164.47	YES(?,O(n^2)) . These rules are removed from the problem. Note that
338.56/164.47	no rule is size-increasing. The overall complexity is obtained by
338.56/164.47	multiplication .
338.56/164.47	
338.56/164.47	Sub-proof:
338.56/164.47	----------
338.56/164.47	  TcT has computed the following triangular matrix interpretation.
338.56/164.47	  
338.56/164.47	    [+](x1, x2) = [1 1] x1 + [1 0] x2 + [0]
338.56/164.47	                  [0 1]      [0 1]      [1]
338.56/164.47	  
338.56/164.47	  The order satisfies the following ordering constraints:
338.56/164.47	  
338.56/164.47	    [+(+(x, y), z)] = [1 2] x + [1 1] y + [1 0] z + [1]
338.56/164.47	                      [0 1]     [0 1]     [0 1]     [2]
338.56/164.47	                    > [1 1] x + [1 1] y + [1 0] z + [0]
338.56/164.47	                      [0 1]     [0 1]     [0 1]     [2]
338.56/164.47	                    = [+(x, +(y, z))]                  
338.56/164.47	                                                       
338.56/164.47	
338.56/164.47	We return to the main proof.
338.56/164.47	
338.56/164.47	We are left with following problem, upon which TcT provides the
338.56/164.47	certificate YES(O(1),O(1)).
338.56/164.47	
338.56/164.47	Rules: Empty
338.56/164.47	Obligation:
338.56/164.47	  derivational complexity
338.56/164.47	Answer:
338.56/164.47	  YES(O(1),O(1))
338.56/164.47	
338.56/164.47	Empty rules are trivially bounded
338.56/164.47	
338.56/164.47	Hurray, we answered YES(O(1),O(n^3))
338.56/164.48	EOF