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