YES(O(1),O(n^2))
12.22/4.97	YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(n^2)).
12.22/4.97	
12.22/4.97	Strict Trs:
12.22/4.97	  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
12.22/4.97	  , *(x, 1()) -> x
12.22/4.97	  , *(+(x, y), z) -> +(*(x, z), *(y, z))
12.22/4.97	  , *(1(), y) -> y }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	We add the following weak dependency pairs:
12.22/4.97	
12.22/4.97	Strict DPs:
12.22/4.97	  { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	  , *^#(x, 1()) -> c_2()
12.22/4.97	  , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
12.22/4.97	  , *^#(1(), y) -> c_4() }
12.22/4.97	
12.22/4.97	and mark the set of starting terms.
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(n^2)).
12.22/4.97	
12.22/4.97	Strict DPs:
12.22/4.97	  { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	  , *^#(x, 1()) -> c_2()
12.22/4.97	  , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
12.22/4.97	  , *^#(1(), y) -> c_4() }
12.22/4.97	Strict Trs:
12.22/4.97	  { *(x, +(y, z)) -> +(*(x, y), *(x, z))
12.22/4.97	  , *(x, 1()) -> x
12.22/4.97	  , *(+(x, y), z) -> +(*(x, z), *(y, z))
12.22/4.97	  , *(1(), y) -> y }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	No rule is usable, rules are removed from the input problem.
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(n^2)).
12.22/4.97	
12.22/4.97	Strict DPs:
12.22/4.97	  { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	  , *^#(x, 1()) -> c_2()
12.22/4.97	  , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z))
12.22/4.97	  , *^#(1(), y) -> c_4() }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	The weightgap principle applies (using the following constant
12.22/4.97	growth matrix-interpretation)
12.22/4.97	
12.22/4.97	The following argument positions are usable:
12.22/4.97	  Uargs(c_1) = {1, 2}, Uargs(c_3) = {1, 2}
12.22/4.97	
12.22/4.97	TcT has computed the following constructor-restricted matrix
12.22/4.97	interpretation.
12.22/4.97	
12.22/4.97	    [+](x1, x2) = [1 2] x1 + [1 2] x2 + [1]
12.22/4.97	                  [0 1]      [0 1]      [1]
12.22/4.97	                                           
12.22/4.97	            [1] = [2]                      
12.22/4.97	                  [1]                      
12.22/4.97	                                           
12.22/4.97	  [*^#](x1, x2) = [0 0] x1 + [0 0] x2 + [1]
12.22/4.97	                  [1 2]      [2 2]      [1]
12.22/4.97	                                           
12.22/4.97	  [c_1](x1, x2) = [1 0] x1 + [1 0] x2 + [1]
12.22/4.97	                  [0 1]      [0 1]      [1]
12.22/4.97	                                           
12.22/4.97	          [c_2] = [0]                      
12.22/4.97	                  [1]                      
12.22/4.97	                                           
12.22/4.97	  [c_3](x1, x2) = [1 0] x1 + [1 0] x2 + [1]
12.22/4.97	                  [0 1]      [0 1]      [1]
12.22/4.97	                                           
12.22/4.97	          [c_4] = [0]                      
12.22/4.97	                  [1]                      
12.22/4.97	
12.22/4.97	The order satisfies the following ordering constraints:
12.22/4.97	
12.22/4.97	  [*^#(x, +(y, z))] = [0 0] x + [0 0] y + [0 0] z + [1]
12.22/4.97	                      [1 2]     [2 6]     [2 6]     [5]
12.22/4.97	                    ? [0 0] x + [0 0] y + [0 0] z + [3]
12.22/4.97	                      [2 4]     [2 2]     [2 2]     [3]
12.22/4.97	                    = [c_1(*^#(x, y), *^#(x, z))]      
12.22/4.97	                                                       
12.22/4.97	      [*^#(x, 1())] = [0 0] x + [1]                    
12.22/4.97	                      [1 2]     [7]                    
12.22/4.97	                    > [0]                              
12.22/4.97	                      [1]                              
12.22/4.97	                    = [c_2()]                          
12.22/4.97	                                                       
12.22/4.97	  [*^#(+(x, y), z)] = [0 0] x + [0 0] y + [0 0] z + [1]
12.22/4.97	                      [1 4]     [1 4]     [2 2]     [4]
12.22/4.97	                    ? [0 0] x + [0 0] y + [0 0] z + [3]
12.22/4.97	                      [1 2]     [1 2]     [4 4]     [3]
12.22/4.97	                    = [c_3(*^#(x, z), *^#(y, z))]      
12.22/4.97	                                                       
12.22/4.97	      [*^#(1(), y)] = [0 0] y + [1]                    
12.22/4.97	                      [2 2]     [5]                    
12.22/4.97	                    > [0]                              
12.22/4.97	                      [1]                              
12.22/4.97	                    = [c_4()]                          
12.22/4.97	                                                       
12.22/4.97	
12.22/4.97	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(n^2)).
12.22/4.97	
12.22/4.97	Strict DPs:
12.22/4.97	  { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	  , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) }
12.22/4.97	Weak DPs:
12.22/4.97	  { *^#(x, 1()) -> c_2()
12.22/4.97	  , *^#(1(), y) -> c_4() }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	The following weak DPs constitute a sub-graph of the DG that is
12.22/4.97	closed under successors. The DPs are removed.
12.22/4.97	
12.22/4.97	{ *^#(x, 1()) -> c_2()
12.22/4.97	, *^#(1(), y) -> c_4() }
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(n^2)).
12.22/4.97	
12.22/4.97	Strict DPs:
12.22/4.97	  { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	  , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	We use the processor 'polynomial interpretation' to orient
12.22/4.97	following rules strictly.
12.22/4.97	
12.22/4.97	DPs:
12.22/4.97	  { 1: *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) }
12.22/4.97	
12.22/4.97	Sub-proof:
12.22/4.97	----------
12.22/4.97	  We consider the following typing:
12.22/4.97	  
12.22/4.97	    + :: (a,a) -> a
12.22/4.97	    *^# :: (a,a) -> b
12.22/4.97	    c_1 :: (b,b) -> b
12.22/4.97	    c_3 :: (b,b) -> b
12.22/4.97	  
12.22/4.97	  The following argument positions are considered usable:
12.22/4.97	  
12.22/4.97	    Uargs(c_1) = {1, 2}, Uargs(c_3) = {1, 2}
12.22/4.97	  
12.22/4.97	  TcT has computed the following constructor-restricted
12.22/4.97	  typedpolynomial interpretation.
12.22/4.97	  
12.22/4.97	    [+](x1, x2) = 2 + x1 + x2   
12.22/4.97	                                
12.22/4.97	  [*^#](x1, x2) = 2*x1*x2 + 2*x2
12.22/4.97	                                
12.22/4.97	  [c_1](x1, x2) = x1 + x2       
12.22/4.97	                                
12.22/4.97	  [c_3](x1, x2) = x1 + x2       
12.22/4.97	                                
12.22/4.97	  
12.22/4.97	  This order satisfies the following ordering constraints.
12.22/4.97	  
12.22/4.97	    [*^#(x, +(y, z))] =  4*x + 2*x*y + 2*x*z + 4 + 2*y + 2*z
12.22/4.97	                      >  2*x*y + 2*y + 2*x*z + 2*z          
12.22/4.97	                      =  [c_1(*^#(x, y), *^#(x, z))]        
12.22/4.97	                                                            
12.22/4.97	    [*^#(+(x, y), z)] =  6*z + 2*x*z + 2*y*z                
12.22/4.97	                      >= 2*x*z + 4*z + 2*y*z                
12.22/4.97	                      =  [c_3(*^#(x, z), *^#(y, z))]        
12.22/4.97	                                                            
12.22/4.97	
12.22/4.97	The strictly oriented rules are moved into the weak component.
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(n^2)).
12.22/4.97	
12.22/4.97	Strict DPs: { *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) }
12.22/4.97	Weak DPs: { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z)) }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(n^2))
12.22/4.97	
12.22/4.97	We use the processor 'polynomial interpretation' to orient
12.22/4.97	following rules strictly.
12.22/4.97	
12.22/4.97	DPs:
12.22/4.97	  { 1: *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) }
12.22/4.97	
12.22/4.97	Sub-proof:
12.22/4.97	----------
12.22/4.97	  We consider the following typing:
12.22/4.97	  
12.22/4.97	    + :: (a,a) -> a
12.22/4.97	    *^# :: (a,a) -> b
12.22/4.97	    c_1 :: (b,b) -> b
12.22/4.97	    c_3 :: (b,b) -> b
12.22/4.97	  
12.22/4.97	  The following argument positions are considered usable:
12.22/4.97	  
12.22/4.97	    Uargs(c_1) = {1, 2}, Uargs(c_3) = {1, 2}
12.22/4.97	  
12.22/4.97	  TcT has computed the following constructor-restricted
12.22/4.97	  typedpolynomial interpretation.
12.22/4.97	  
12.22/4.97	    [+](x1, x2) = 1 + x1 + x2 
12.22/4.97	                              
12.22/4.97	  [*^#](x1, x2) = x1 + 2*x1*x2
12.22/4.97	                              
12.22/4.97	  [c_1](x1, x2) = x1 + x2     
12.22/4.97	                              
12.22/4.97	  [c_3](x1, x2) = x1 + x2     
12.22/4.97	                              
12.22/4.97	  
12.22/4.97	  This order satisfies the following ordering constraints.
12.22/4.97	  
12.22/4.97	    [*^#(x, +(y, z))] =  3*x + 2*x*y + 2*x*z            
12.22/4.97	                      >= 2*x + 2*x*y + 2*x*z            
12.22/4.97	                      =  [c_1(*^#(x, y), *^#(x, z))]    
12.22/4.97	                                                        
12.22/4.97	    [*^#(+(x, y), z)] =  1 + x + y + 2*z + 2*x*z + 2*y*z
12.22/4.97	                      >  x + 2*x*z + y + 2*y*z          
12.22/4.97	                      =  [c_3(*^#(x, z), *^#(y, z))]    
12.22/4.97	                                                        
12.22/4.97	
12.22/4.97	The strictly oriented rules are moved into the weak component.
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(1)).
12.22/4.97	
12.22/4.97	Weak DPs:
12.22/4.97	  { *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	  , *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) }
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(1))
12.22/4.97	
12.22/4.97	The following weak DPs constitute a sub-graph of the DG that is
12.22/4.97	closed under successors. The DPs are removed.
12.22/4.97	
12.22/4.97	{ *^#(x, +(y, z)) -> c_1(*^#(x, y), *^#(x, z))
12.22/4.97	, *^#(+(x, y), z) -> c_3(*^#(x, z), *^#(y, z)) }
12.22/4.97	
12.22/4.97	We are left with following problem, upon which TcT provides the
12.22/4.97	certificate YES(O(1),O(1)).
12.22/4.97	
12.22/4.97	Rules: Empty
12.22/4.97	Obligation:
12.22/4.97	  innermost runtime complexity
12.22/4.97	Answer:
12.22/4.97	  YES(O(1),O(1))
12.22/4.97	
12.22/4.97	Empty rules are trivially bounded
12.22/4.97	
12.22/4.97	Hurray, we answered YES(O(1),O(n^2))
12.22/4.98	EOF