YES(O(1),O(n^1))
0.00/0.79	YES(O(1),O(n^1))
0.00/0.79	
0.00/0.79	We are left with following problem, upon which TcT provides the
0.00/0.79	certificate YES(O(1),O(n^1)).
0.00/0.79	
0.00/0.79	Strict Trs:
0.00/0.79	  { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z))
0.00/0.79	  , times(X, s(Y)) -> plus(X, times(Y, X)) }
0.00/0.79	Obligation:
0.00/0.79	  runtime complexity
0.00/0.79	Answer:
0.00/0.79	  YES(O(1),O(n^1))
0.00/0.79	
0.00/0.79	The weightgap principle applies (using the following nonconstant
0.00/0.79	growth matrix-interpretation)
0.00/0.79	
0.00/0.79	The following argument positions are usable:
0.00/0.79	  Uargs(plus) = {2}
0.00/0.79	
0.00/0.79	TcT has computed the following matrix interpretation satisfying
0.00/0.79	not(EDA) and not(IDA(1)).
0.00/0.79	
0.00/0.79	   [plus](x1, x2) = [1] x2 + [5]         
0.00/0.79	                                         
0.00/0.79	  [times](x1, x2) = [1] x1 + [1] x2 + [7]
0.00/0.79	                                         
0.00/0.79	          [s](x1) = [1] x1 + [7]         
0.00/0.79	
0.00/0.79	The order satisfies the following ordering constraints:
0.00/0.79	
0.00/0.79	  [plus(plus(X, Y), Z)] = [1] Z + [5]           
0.00/0.79	                        ? [1] Z + [10]          
0.00/0.79	                        = [plus(X, plus(Y, Z))] 
0.00/0.79	                                                
0.00/0.79	       [times(X, s(Y))] = [1] X + [1] Y + [14]  
0.00/0.79	                        > [1] X + [1] Y + [12]  
0.00/0.79	                        = [plus(X, times(Y, X))]
0.00/0.79	                                                
0.00/0.79	
0.00/0.79	Further, it can be verified that all rules not oriented are covered by the weightgap condition.
0.00/0.79	
0.00/0.79	We are left with following problem, upon which TcT provides the
0.00/0.79	certificate YES(O(1),O(n^1)).
0.00/0.79	
0.00/0.79	Strict Trs: { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)) }
0.00/0.79	Weak Trs: { times(X, s(Y)) -> plus(X, times(Y, X)) }
0.00/0.79	Obligation:
0.00/0.79	  runtime complexity
0.00/0.79	Answer:
0.00/0.79	  YES(O(1),O(n^1))
0.00/0.79	
0.00/0.79	We use the processor 'matrix interpretation of dimension 2' to
0.00/0.79	orient following rules strictly.
0.00/0.79	
0.00/0.79	Trs: { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z)) }
0.00/0.79	
0.00/0.79	The induced complexity on above rules (modulo remaining rules) is
0.00/0.79	YES(?,O(n^1)) . These rules are moved into the corresponding weak
0.00/0.79	component(s).
0.00/0.79	
0.00/0.79	Sub-proof:
0.00/0.79	----------
0.00/0.79	  The following argument positions are usable:
0.00/0.79	    Uargs(plus) = {2}
0.00/0.79	  
0.00/0.79	  TcT has computed the following constructor-based matrix
0.00/0.79	  interpretation satisfying not(EDA) and not(IDA(1)).
0.00/0.79	  
0.00/0.79	     [plus](x1, x2) = [0 1] x1 + [1 0] x2 + [0]
0.00/0.79	                      [0 1]      [0 1]      [4]
0.00/0.79	                                               
0.00/0.79	    [times](x1, x2) = [1 1] x1 + [1 0] x2 + [1]
0.00/0.79	                      [1 1]      [1 0]      [1]
0.00/0.79	                                               
0.00/0.79	            [s](x1) = [1 1] x1 + [7]           
0.00/0.79	                      [0 0]      [0]           
0.00/0.79	  
0.00/0.79	  The order satisfies the following ordering constraints:
0.00/0.79	  
0.00/0.79	    [plus(plus(X, Y), Z)] = [0 1] X + [0 1] Y + [1 0] Z + [4]
0.00/0.79	                            [0 1]     [0 1]     [0 1]     [8]
0.00/0.79	                          > [0 1] X + [0 1] Y + [1 0] Z + [0]
0.00/0.79	                            [0 1]     [0 1]     [0 1]     [8]
0.00/0.79	                          = [plus(X, plus(Y, Z))]            
0.00/0.79	                                                             
0.00/0.79	         [times(X, s(Y))] = [1 1] X + [1 1] Y + [8]          
0.00/0.79	                            [1 1]     [1 1]     [8]          
0.00/0.79	                          > [1 1] X + [1 1] Y + [1]          
0.00/0.79	                            [1 1]     [1 1]     [5]          
0.00/0.79	                          = [plus(X, times(Y, X))]           
0.00/0.79	                                                             
0.00/0.79	
0.00/0.79	We return to the main proof.
0.00/0.79	
0.00/0.79	We are left with following problem, upon which TcT provides the
0.00/0.79	certificate YES(O(1),O(1)).
0.00/0.79	
0.00/0.79	Weak Trs:
0.00/0.79	  { plus(plus(X, Y), Z) -> plus(X, plus(Y, Z))
0.00/0.79	  , times(X, s(Y)) -> plus(X, times(Y, X)) }
0.00/0.79	Obligation:
0.00/0.79	  runtime complexity
0.00/0.79	Answer:
0.00/0.79	  YES(O(1),O(1))
0.00/0.79	
0.00/0.79	Empty rules are trivially bounded
0.00/0.79	
0.00/0.79	Hurray, we answered YES(O(1),O(n^1))
0.00/0.80	EOF