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